Theorem axc16nfALT

Description: Alternate proof of axc16nf , shorter but requiring ax-11 and ax-13 . (Contributed by Mario Carneiro, 7-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axc16nfALT	$$⊢\forall xx=y\to Ⅎz\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfae	$$⊢Ⅎz\forall xx=y$$
2		axc16g	$$⊢\forall xx=y\to \left(\phi \to \forall z\phi \right)$$
3	1 2	nf5d	$$⊢\forall xx=y\to Ⅎz\phi$$