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  2108  ax16g-o  2266  axc11-o  2283  trint0  4549  onfununi  7004  smoiun  7024  findcard2  7752  findcard3  7755  inficl  7877  en3lplem2  8023  r1sdom  8183  infxpenlem  8382  alephordi  8446  cardaleph  8461  pwsdompw  8575  cfslb2n  8639  isf32lem10  8733  axdc4lem  8826  zorn2lem2  8868  alephreg  8948  inar1  9142  tskuni  9150  grudomon  9184  nqereu  9296  ltleletr  9666  elfz0ubfz0  11782  ssnn0fi  12076  caubnd  13273  sqreulem  13274  bezoutlem1  14260  pcprendvds  14448  prmreclem3  14520  ptcmpfi  20480  ufilen  20597  fcfnei  20702  bcthlem5  21933  aaliou  22900  cusgrarn  24661  3cyclfrgrarn1  25214  n4cyclfrgra  25220  occon2  26404  occon3  26413  atexch  27498  sigaclci  28362  frmin  29562  idinside  29962  heibor1lem  30545  aomclem2  31240  leltletr  32692  ee02  33610  tratrb  33697  trsspwALT2  34011
  Copyright terms: Public domain W3C validator