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  2079  ax16g-o  2257  axc11-o  2274  trint0  4557  onfununi  7013  smoiun  7033  findcard2  7761  findcard3  7764  inficl  7886  en3lplem2  8033  r1sdom  8193  infxpenlem  8392  alephordi  8456  cardaleph  8471  pwsdompw  8585  cfslb2n  8649  isf32lem10  8743  axdc4lem  8836  zorn2lem2  8878  alephreg  8958  inar1  9154  tskuni  9162  grudomon  9196  nqereu  9308  ltleletr  9678  elfz0ubfz0  11777  ssnn0fi  12063  caubnd  13157  sqreulem  13158  bezoutlem1  14038  pcprendvds  14226  prmreclem3  14298  ptcmpfi  20141  ufilen  20258  fcfnei  20363  bcthlem5  21594  aaliou  22560  cusgrarn  24232  3cyclfrgrarn1  24785  n4cyclfrgra  24791  occon2  25979  occon3  25988  atexch  27073  sigaclci  27883  frmin  29175  idinside  29587  heibor1lem  30135  aomclem2  30832  leltletr  32012  ee02  32519  tratrb  32603  trsspwALT2  32914
  Copyright terms: Public domain W3C validator