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	⊢ ( ¬ 𝑥 = 𝑥 → ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.21	⊢ ( ¬ 𝑥 = 𝑥 → ( 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) )