Theorem alim ≪ | index | src | ≫

theorem alim {x: nat} (p q: wff x): $ A. x (p -> q) -> A. x p -> A. x q $;

Step	Hyp	Ref	Expression
1		ax_4	A. x (p -> q) -> A. x p -> A. x q

Axiom use

axs_pred_calc (ax_4)