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

Theorem sylsyld 52
Description: Virtual deduction rule e12 28499 without virtual deduction symbols. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
sylsyld.1  |-  ( ph  ->  ps )
sylsyld.2  |-  ( ph  ->  ( ch  ->  th )
)
sylsyld.3  |-  ( ps 
->  ( th  ->  ta ) )
Assertion
Ref Expression
sylsyld  |-  ( ph  ->  ( ch  ->  ta ) )

Proof of Theorem sylsyld
StepHypRef Expression
1 sylsyld.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
2 sylsyld.1 . . 3  |-  ( ph  ->  ps )
3 sylsyld.3 . . 3  |-  ( ps 
->  ( th  ->  ta ) )
42, 3syl 15 . 2  |-  ( ph  ->  ( th  ->  ta ) )
51, 4syld 40 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ee02  1367  ax10o  1892  a16gALT  1989  a16g-o  2125  ax10o-o  2142  trint0  4130  onfununi  6358  smoiun  6378  tfrlem2  6392  findcard2  7098  findcard3  7100  inficl  7178  en3lplem2  7417  infxpenlem  7641  cardaleph  7716  pwsdompw  7830  cfslb2n  7894  isf32lem10  7988  axdc4lem  8081  zorn2lem2  8124  alephreg  8204  inar1  8397  tskuni  8405  grudomon  8439  nqereu  8553  caubnd  11842  sqreulem  11843  bezoutlem1  12717  pcprendvds  12893  prmreclem3  12965  ptcmpfi  17504  ufilen  17625  fcfnei  17730  bcthlem5  18750  aaliou  19718  occon2  21867  occon3  21876  atexch  22961  frmin  24242  idinside  24707  carinttar  25902  lineval6a  26089  heibor1lem  26533  aomclem2  27152  tratrb  28299  trsspwALT2  28593
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator