Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axc11-o Structured version   Unicode version

Theorem axc11-o 31955
Description: Show that ax-c11 31892 can be derived from ax-c11n 31893. An open problem is whether this theorem can be derived from ax-c11n 31893 and the others when ax-12 1878 is replaced with ax-c15 31894. See theorem axc11nfromc11 31930 for the rederivation of ax-c11n 31893 from axc11 2080.

Normally, axc11 2080 should be used rather than ax-c11 31892 or axc11-o 31955, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion
Ref Expression
axc11-o  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)

Proof of Theorem axc11-o
StepHypRef Expression
1 ax-c11n 31893 . 2  |-  ( A. x  x  =  y  ->  A. y  y  =  x )
2 ax12 31908 . . . 4  |-  ( y  =  x  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
32equcoms 1819 . . 3  |-  ( x  =  y  ->  ( A. x ph  ->  A. y
( y  =  x  ->  ph ) ) )
43sps-o 31912 . 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 1657 . 2  |-  ( A. y  y  =  x  ->  ( A. y ( y  =  x  ->  ph )  ->  A. y ph ) )
71, 4, 6sylsyld 55 1  |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-11 1866  ax-c5 31888  ax-c4 31889  ax-c7 31890  ax-c11 31892  ax-c11n 31893  ax-c15 31894  ax-c9 31895
This theorem depends on definitions:  df-bi 185  df-ex 1634
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator