Metamath Proof Explorer

Theorem ax13ALT

Description: Alternate proof of ax13 from FOL, sp , and axc9 . (Contributed by NM, 21-Dec-2015) (Proof shortened by Wolf Lammen, 31-Jan-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax13ALT ⊢ ¬ x = y → y = z → ∀ x y = z

Proof

Step Hyp Ref Expression
1 sp ⊢ ∀ x x = y → x = y
2 1 con3i ⊢ ¬ x = y → ¬ ∀ x x = y
3 sp ⊢ ∀ x x = z → x = z
4 3 con3i ⊢ ¬ x = z → ¬ ∀ x x = z
5 axc9 ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → y = z → ∀ x y = z
6 2 4 5 syl2im ⊢ ¬ x = y → ¬ x = z → y = z → ∀ x y = z
7 ax13b ⊢ ¬ x = y → y = z → ∀ x y = z ↔ ¬ x = y → ¬ x = z → y = z → ∀ x y = z
8 6 7 mpbir ⊢ ¬ x = y → y = z → ∀ x y = z