New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax12bOLD GIF version

Theorem ax12bOLD 1690
 Description: Obsolete version of ax12b 1689 as of 12-Aug-2017. (Contributed by NM, 2-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax12bOLD ((¬ x = y → (y = zx y = z)) ↔ (¬ x = y → (¬ x = z → (y = zx y = z))))

Proof of Theorem ax12bOLD
StepHypRef Expression
1 bi2.04 350 . . . 4 ((¬ x = y → (y = zx y = z)) ↔ (y = z → (¬ x = yx y = z)))
2 equtrr 1683 . . . . . . . . 9 (z = y → (x = zx = y))
32equcoms 1681 . . . . . . . 8 (y = z → (x = zx = y))
43con3d 125 . . . . . . 7 (y = z → (¬ x = y → ¬ x = z))
54pm4.71d 615 . . . . . 6 (y = z → (¬ x = y ↔ (¬ x = y ¬ x = z)))
65imbi1d 308 . . . . 5 (y = z → ((¬ x = yx y = z) ↔ ((¬ x = y ¬ x = z) → x y = z)))
76pm5.74i 236 . . . 4 ((y = z → (¬ x = yx y = z)) ↔ (y = z → ((¬ x = y ¬ x = z) → x y = z)))
81, 7bitri 240 . . 3 ((¬ x = y → (y = zx y = z)) ↔ (y = z → ((¬ x = y ¬ x = z) → x y = z)))
9 bi2.04 350 . . 3 ((y = z → ((¬ x = y ¬ x = z) → x y = z)) ↔ ((¬ x = y ¬ x = z) → (y = zx y = z)))
108, 9bitri 240 . 2 ((¬ x = y → (y = zx y = z)) ↔ ((¬ x = y ¬ x = z) → (y = zx y = z)))
11 impexp 433 . 2 (((¬ x = y ¬ x = z) → (y = zx y = z)) ↔ (¬ x = y → (¬ x = z → (y = zx y = z))))
1210, 11bitri 240 1 ((¬ x = y → (y = zx y = z)) ↔ (¬ x = y → (¬ x = z → (y = zx y = z))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator