Theorem alcom ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		ax_11	A. x A. y p -> A. y A. x p

Axiom use

axs_pred_calc (ax_11)