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

Theorem sylsyld 56
Description: A double syllogism inference. (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 44 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  axc16gALT  2056  ax16g-o  2235  axc11-o  2252  trint0  4423  onfununi  6823  smoiun  6843  findcard2  7573  findcard3  7576  inficl  7696  en3lplem2  7842  r1sdom  8002  infxpenlem  8201  alephordi  8265  cardaleph  8280  pwsdompw  8394  cfslb2n  8458  isf32lem10  8552  axdc4lem  8645  zorn2lem2  8687  alephreg  8767  inar1  8963  tskuni  8971  grudomon  9005  nqereu  9119  ltleletr  9488  elfzelfzelfz  11505  caubnd  12867  sqreulem  12868  bezoutlem1  13743  pcprendvds  13928  prmreclem3  14000  ptcmpfi  19408  ufilen  19525  fcfnei  19630  bcthlem5  20861  aaliou  21826  cusgrarn  23389  occon2  24713  occon3  24722  atexch  25807  sigaclci  26597  frmin  27725  idinside  28137  heibor1lem  28734  aomclem2  29434  leltletr  30199  3cyclfrgrarn1  30630  n4cyclfrgra  30636  ssnn0fi  30775  ee02  31254  tratrb  31338  trsspwALT2  31649
  Copyright terms: Public domain W3C validator