Theorem ial ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		ax_5	p -> A. x p

Axiom use

axs_pred_calc (ax_5)