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

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

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