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

Theorem ax10o 1905
Description: Show that ax-10o 2091 can be derived from ax-10 2092 in the form of ax10 1897. Normally, ax10o 1905 should be used rather than ax-10o 2091, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.)
Assertion
Ref Expression
ax10o  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)

Proof of Theorem ax10o
StepHypRef Expression
1 ax10 1897 . 2  |-  ( A. x  x  =  y  ->  A. y  y  =  x )
2 ax-11 1727 . . . 4  |-  ( y  =  x  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
32equcoms 1666 . . 3  |-  ( x  =  y  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
43sps 1751 . 2  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ( y  =  x  ->  ph )
) )
5 pm2.27 35 . . 3  |-  ( y  =  x  ->  (
( y  =  x  ->  ph )  ->  ph )
)
65al2imi 1551 . 2  |-  ( A. y  y  =  x  ->  ( A. y ( y  =  x  ->  ph )  ->  A. y ph ) )
71, 4, 6sylsyld 52 1  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  hbae  1906  dvelimh  1917  dral1  1918  nd1  8225  nd2  8226  axpowndlem3  8237  a9e2eq  28622  a9e2eqVD  28999  2sb5ndVD  29002  2sb5ndALT  29025  a12stdy1  29748  a12stdy2  29749  a12stdy4  29751
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator