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

Theorem ax10o 1896
Description: Show that ax-10o 2083 can be derived from ax-10 2084 in the form of ax10 1888. Normally, ax10o 1896 should be used rather than ax-10o 2083, 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 1888 . 2  |-  ( A. x  x  =  y  ->  A. y  y  =  x )
2 ax-11 1718 . . . 4  |-  ( y  =  x  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
32equcoms 1654 . . 3  |-  ( x  =  y  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
43sps 1743 . 2  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ( y  =  x  ->  ph )
) )
5 pm2.27 37 . . 3  |-  ( y  =  x  ->  (
( y  =  x  ->  ph )  ->  ph )
)
65al2imi 1550 . 2  |-  ( A. y  y  =  x  ->  ( A. y ( y  =  x  ->  ph )  ->  A. y ph ) )
71, 4, 6sylsyld 54 1  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1529
This theorem is referenced by:  hbae  1897  dvelimfALT  1909  dral1  1910  nd1  8206  nd2  8207  axpowndlem3  8218  a9e2eq  27596  a9e2eqVD  27953  2sb5ndVD  27956  2sb5ndALT  27979  a12stdy1  28395  a12stdy2  28396  a12stdy4  28398
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1531
  Copyright terms: Public domain W3C validator