Theorem ax12v 1926

Description: A weaker version of ax-12 1925 with distinct variable restrictions on pairs x, z and y, z. In order to show that this weakening is adequate, this should be the only theorem referencing ax-12 1925 directly. (Contributed by NM, 30-Jun-2016.)

Assertion

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

Distinct variable groups:   x,z   y,z

Proof of Theorem ax12v

Step	Hyp	Ref	Expression
1		ax-12 1925	1 ⊢ (¬ x = y → (y = z → ∀x y = z))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-12 1925

This theorem is referenced by:  ax12o  1934