Theorem ax12olem3 1929

Description: Lemma for ax12o 1934. Show the equivalence of an intermediate equivalent to ax12o 1934 with the conjunction of ax-12 1925 and a variant with negated equalities. (Contributed by NM, 24-Dec-2015.)

Assertion

Ref	Expression
ax12olem3	⊢ ((¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)) ↔ ((¬ x = y → (y = z → ∀x y = z)) ∧ (¬ x = y → (¬ y = z → ∀x ¬ y = z))))

Proof of Theorem ax12olem3

Step	Hyp	Ref	Expression
1		sp 1747	. . . . . 6 ⊢ (∀x ¬ y = z → ¬ y = z)
2	1	con2i 112	. . . . 5 ⊢ (y = z → ¬ ∀x ¬ y = z)
3	2	imim1i 54	. . . 4 ⊢ ((¬ ∀x ¬ y = z → ∀x y = z) → (y = z → ∀x y = z))
4	3	imim2i 13	. . 3 ⊢ ((¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)) → (¬ x = y → (y = z → ∀x y = z)))
5		sp 1747	. . . . . 6 ⊢ (∀x y = z → y = z)
6	5	imim2i 13	. . . . 5 ⊢ ((¬ ∀x ¬ y = z → ∀x y = z) → (¬ ∀x ¬ y = z → y = z))
7	6	con1d 116	. . . 4 ⊢ ((¬ ∀x ¬ y = z → ∀x y = z) → (¬ y = z → ∀x ¬ y = z))
8	7	imim2i 13	. . 3 ⊢ ((¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)) → (¬ x = y → (¬ y = z → ∀x ¬ y = z)))
9	4, 8	jca 518	. 2 ⊢ ((¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)) → ((¬ x = y → (y = z → ∀x y = z)) ∧ (¬ x = y → (¬ y = z → ∀x ¬ y = z))))
10		con1 120	. . . . . 6 ⊢ ((¬ y = z → ∀x ¬ y = z) → (¬ ∀x ¬ y = z → y = z))
11	10	imim1d 69	. . . . 5 ⊢ ((¬ y = z → ∀x ¬ y = z) → ((y = z → ∀x y = z) → (¬ ∀x ¬ y = z → ∀x y = z)))
12	11	com12 27	. . . 4 ⊢ ((y = z → ∀x y = z) → ((¬ y = z → ∀x ¬ y = z) → (¬ ∀x ¬ y = z → ∀x y = z)))
13	12	imim3i 55	. . 3 ⊢ ((¬ x = y → (y = z → ∀x y = z)) → ((¬ x = y → (¬ y = z → ∀x ¬ y = z)) → (¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z))))
14	13	imp 418	. 2 ⊢ (((¬ x = y → (y = z → ∀x y = z)) ∧ (¬ x = y → (¬ y = z → ∀x ¬ y = z))) → (¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)))
15	9, 14	impbii 180	1 ⊢ ((¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)) ↔ ((¬ x = y → (y = z → ∀x y = z)) ∧ (¬ x = y → (¬ 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  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542

This theorem is referenced by:  ax12olem4  1930