Metamath Proof Explorer


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