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 28813 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  1905  a16gALT  2002  a16g-o  2138  ax10o-o  2155  trint0  4146  onfununi  6374  smoiun  6394  tfrlem2  6408  findcard2  7114  findcard3  7116  inficl  7194  en3lplem2  7433  infxpenlem  7657  cardaleph  7732  pwsdompw  7846  cfslb2n  7910  isf32lem10  8004  axdc4lem  8097  zorn2lem2  8140  alephreg  8220  inar1  8413  tskuni  8421  grudomon  8455  nqereu  8569  caubnd  11858  sqreulem  11859  bezoutlem1  12733  pcprendvds  12909  prmreclem3  12981  ptcmpfi  17520  ufilen  17641  fcfnei  17746  bcthlem5  18766  aaliou  19734  occon2  21883  occon3  21892  atexch  22977  frmin  24313  idinside  24779  carinttar  26005  lineval6a  26192  heibor1lem  26636  aomclem2  27255  3cyclfrgrarn1  28435  n4cyclfrgra  28440  tratrb  28598  trsspwALT2  28909  ax10oNEW7  29453  ax7w1hAUX7  29616  a16gALTOLD7  29698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator