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 = z → ∀x y = z)) ↔ (¬ x = y → (¬ x = z → (y = z → ∀x y = z))))

Proof of Theorem ax12bOLD

Step	Hyp	Ref	Expression
1		bi2.04 350	. . . 4 ⊢ ((¬ x = y → (y = z → ∀x y = z)) ↔ (y = z → (¬ x = y → ∀x y = z)))
2		equtrr 1683	. . . . . . . . 9 ⊢ (z = y → (x = z → x = y))
3	2	equcoms 1681	. . . . . . . 8 ⊢ (y = z → (x = z → x = y))
4	3	con3d 125	. . . . . . 7 ⊢ (y = z → (¬ x = y → ¬ x = z))
5	4	pm4.71d 615	. . . . . 6 ⊢ (y = z → (¬ x = y ↔ (¬ x = y ∧ ¬ x = z)))
6	5	imbi1d 308	. . . . 5 ⊢ (y = z → ((¬ x = y → ∀x y = z) ↔ ((¬ x = y ∧ ¬ x = z) → ∀x y = z)))
7	6	pm5.74i 236	. . . 4 ⊢ ((y = z → (¬ x = y → ∀x y = z)) ↔ (y = z → ((¬ x = y ∧ ¬ x = z) → ∀x y = z)))
8	1, 7	bitri 240	. . 3 ⊢ ((¬ x = y → (y = z → ∀x 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 = z → ∀x y = z)))
10	8, 9	bitri 240	. 2 ⊢ ((¬ x = y → (y = z → ∀x y = z)) ↔ ((¬ x = y ∧ ¬ x = z) → (y = z → ∀x y = z)))
11		impexp 433	. 2 ⊢ (((¬ x = y ∧ ¬ x = z) → (y = z → ∀x y = z)) ↔ (¬ x = y → (¬ x = z → (y = z → ∀x y = z))))
12	10, 11	bitri 240	1 ⊢ ((¬ x = y → (y = z → ∀x y = z)) ↔ (¬ x = y → (¬ x = z → (y = z → ∀x y = z))))

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)