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

Theorem ax10o 1892
Description: Show that ax-10o 2078 can be derived from ax-10 2079 in the form of ax10 1884. Normally, ax10o 1892 should be used rather than ax-10o 2078, 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 1884 . 2  |-  ( A. x  x  =  y  ->  A. y  y  =  x )
2 ax-11 1715 . . . 4  |-  ( y  =  x  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
32equcoms 1651 . . 3  |-  ( x  =  y  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
43sps 1739 . 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 1548 . 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 1527
This theorem is referenced by:  hbae  1893  dvelimh  1904  dral1  1905  nd1  8209  nd2  8210  axpowndlem3  8221  a9e2eq  28323  a9e2eqVD  28683  2sb5ndVD  28686  2sb5ndALT  28709  a12stdy1  29126  a12stdy2  29127  a12stdy4  29129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator