Theorem pimeq | index | src |

theorem pimeq (p q: wff) {x: nat}: $ (P. x p -> q) -> A. x (p -> q) $;
StepHypRefExpression
1 anr
E. x p /\ A. x (p -> q) -> A. x (p -> q)
2 1 conv pim
(P. x p -> q) -> A. x (p -> q)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)