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 -> A.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 -> A.x y = z))

Syntax hints:  -. wn 3   -> wi 4  A.wal 1540

This theorem was proved from axioms:  ax-12 1925

This theorem is referenced by:  ax12o  1934