Metamath Proof Explorer


Theorem ax13fromc9

Description: Derive ax-13 from ax-c9 and other older axioms.

This proof uses newer axioms ax-4 and ax-6 , but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 and ax-c10 . (Contributed by NM, 21-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax13fromc9 ¬ x = y y = z x y = z

Proof

Step Hyp Ref Expression
1 ax-c5 x x = y x = y
2 1 con3i ¬ x = y ¬ x x = y
3 ax-c5 x x = z x = z
4 3 con3i ¬ x = z ¬ x x = z
5 ax-c9 ¬ 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