Theorem a12stdy4 1373

Description: Part of a study related to ax-12 966. The second antecedent of ax-12 966 is replaced. There are no distinct variable restrictions.

Assertion

Ref	Expression
a12stdy4	⊢ (¬ ∀z z = x → (∀y z = x → (x = y → ∀z x = y)))

Proof of Theorem a12stdy4

Step	Hyp	Ref	Expression
1		ax-10o 1138	. . . . . . 7 ⊢ (∀y y = z → (∀y z = x → ∀z z = x))
2	1	alequcoms 1141	. . . . . 6 ⊢ (∀z z = y → (∀y z = x → ∀z z = x))
3	2	con3d 95	. . . . 5 ⊢ (∀z z = y → (¬ ∀z z = x → ¬ ∀y z = x))
4	3	impcom 351	. . . 4 ⊢ ((¬ ∀z z = x ⋀ ∀z z = y) → ¬ ∀y z = x)
5	4	pm2.21d 78	. . 3 ⊢ ((¬ ∀z z = x ⋀ ∀z z = y) → (∀y z = x → (x = y → ∀z x = y)))
6	5	ex 373	. 2 ⊢ (¬ ∀z z = x → (∀z z = y → (∀y z = x → (x = y → ∀z x = y))))
7		ax-12 966	. . 3 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
8	7	a1dd 42	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (∀y z = x → (x = y → ∀z x = y))))
9	6, 8	pm2.61d 127	1 ⊢ (¬ ∀z z = x → (∀y z = x → (x = y → ∀z x = y)))

Syntax hints:  ¬ wn 2   → wi 3   ⋀ wa 223  ∀wal 952   = wceq 954

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-10 964  ax-12 966  ax-10o 1138

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain