Theorem nfri ≪ | index | src | ≫

theorem nfri {x: nat} (a: wff x): $ a -> A. x a $ > $ F/ x a $;

Step	Hyp	Ref	Expression
1		hyp h	a -> A. x a
2	1	ax_gen	A. x (a -> A. x a)
3	2	conv nf	F/ x a

Axiom use

axs_pred_calc (ax_gen)