MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax12w Unicode version

Theorem ax12w 1698
Description: Weak version (principal instance) of ax-12 1866 not involving bundling. Uses only Tarski's FOL axiom schemes. The proof is trivial but is included to complete the set ax6w 1691, ax7w 1692, and ax11w 1695. (Contributed by NM, 10-Apr-2017.)
Assertion
Ref Expression
ax12w  |-  ( -.  x  =  y  -> 
( y  =  z  ->  A. x  y  =  z ) )
Distinct variable group:    x, y, z

Proof of Theorem ax12w
StepHypRef Expression
1 a17d 1604 1  |-  ( -.  x  =  y  -> 
( y  =  z  ->  A. x  y  =  z ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527
This theorem was proved from axioms:  ax-1 5  ax-mp 8  ax-17 1603
  Copyright terms: Public domain W3C validator