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

Theorem ax10o 2001
Description: Show that ax-10o 2189 can be derived from ax-10 2190 in the form of ax10 1991. Normally, ax10o 2001 should be used rather than ax-10o 2189, 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 1991 . 2  |-  ( A. x  x  =  y  ->  A. y  y  =  x )
2 ax-11 1757 . . . 4  |-  ( y  =  x  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
32equcoms 1689 . . 3  |-  ( x  =  y  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
43sps 1766 . 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 1567 . 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 4   A.wal 1546
This theorem is referenced by:  hbae  2005  a16g  2012  dvelimh  2015  dvelimhOLD  2016  dral1  2022  dral1OLD  2023  nd1  8418  nd2  8419  axpowndlem3  8430  a9e2eq  28355  a9e2eqVD  28728  2sb5ndVD  28731  2sb5ndALT  28754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator