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:  ee02  1421  ax16gALT  2105  ax16g-o  2236  axc11-o  2253  trint0  4390  onfununi  6788  smoiun  6808  findcard2  7540  findcard3  7543  inficl  7663  en3lplem2  7809  infxpenlem  8168  cardaleph  8247  pwsdompw  8361  cfslb2n  8425  isf32lem10  8519  axdc4lem  8612  zorn2lem2  8654  alephreg  8734  inar1  8929  tskuni  8937  grudomon  8971  nqereu  9085  ltleletr  9454  elfzelfzelfz  11470  caubnd  12829  sqreulem  12830  bezoutlem1  13704  pcprendvds  13889  prmreclem3  13961  ptcmpfi  19227  ufilen  19344  fcfnei  19449  bcthlem5  20680  aaliou  21688  cusgrarn  23189  occon2  24513  occon3  24522  atexch  25607  sigaclci  26428  frmin  27549  idinside  27961  heibor1lem  28549  aomclem2  29250  leltletr  30016  3cyclfrgrarn1  30447  n4cyclfrgra  30453  tratrb  30940  trsspwALT2  31252
  Copyright terms: Public domain W3C validator