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

Theorem sylsyld 55
Description: Virtual deduction rule e12 28898 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 16 . 2  |-  ( ph  ->  ( th  ->  ta ) )
51, 4syld 43 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ee02  1387  ax10oOLD  2040  a16gALT  2158  a16g-o  2265  ax10o-o  2282  trint0  4321  onfununi  6605  smoiun  6625  tfrlem2  6639  findcard2  7350  findcard3  7352  inficl  7432  en3lplem2  7673  infxpenlem  7897  cardaleph  7972  pwsdompw  8086  cfslb2n  8150  isf32lem10  8244  axdc4lem  8337  zorn2lem2  8379  alephreg  8459  inar1  8652  tskuni  8660  grudomon  8694  nqereu  8808  caubnd  12164  sqreulem  12165  bezoutlem1  13040  pcprendvds  13216  prmreclem3  13288  ptcmpfi  17847  ufilen  17964  fcfnei  18069  bcthlem5  19283  aaliou  20257  cusgrarn  21470  occon2  22792  occon3  22801  atexch  23886  sigaclci  24517  frmin  25519  idinside  26020  heibor1lem  26520  aomclem2  27132  elfzelfzelfz  28120  3cyclfrgrarn1  28464  n4cyclfrgra  28470  tratrb  28682  trsspwALT2  28994  ax10oNEW7  29538  ax7w1hAUX7  29708  a16gALTOLD7  29806
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator