Theorem ax13dgen4

Description: Degenerate instance of ax-13 where bundled variables x , y , and z have a common substitution. Therefore, also a degenerate instance of ax13dgen1 , ax13dgen2 , and ax13dgen3 . Also an instance of the intuitionistic tautology pm2.21 . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017) Reduce axiom usage. (Revised by Wolf Lammen, 10-Oct-2021)

	Ref	Expression
Assertion	ax13dgen4	$$⊢\neg x=x\to \left(x=x\to \forall xx=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2.21	$$⊢\neg x=x\to \left(x=x\to \forall xx=x\right)$$