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

Theorem sylsyld 61
Description: A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
sylsyld.1 (𝜑𝜓)
sylsyld.2 (𝜑 → (𝜒𝜃))
sylsyld.3 (𝜓 → (𝜃𝜏))
Assertion
Ref Expression
sylsyld (𝜑 → (𝜒𝜏))

Proof of Theorem sylsyld
StepHypRef Expression
1 sylsyld.2 . 2 (𝜑 → (𝜒𝜃))
2 sylsyld.1 . . 3 (𝜑𝜓)
3 sylsyld.3 . . 3 (𝜓 → (𝜃𝜏))
42, 3syl 17 . 2 (𝜑 → (𝜃𝜏))
51, 4syld 47 1 (𝜑 → (𝜒𝜏))
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:  mpsylsyld  69  syl6an  683  axc16gALT  2511  rspc2vd  3880  trintss  5156  onfununi  7965  smoiun  7985  findcard2  8746  findcard3  8749  inficl  8877  en3lplem2  9064  infxpenlem  9428  alephordi  9489  cardaleph  9504  pwsdompw  9619  cfslb2n  9683  isf32lem10  9777  axdc4lem  9870  zorn2lem2  9912  alephreg  9997  inar1  10190  tskuni  10198  grudomon  10232  nqereu  10344  ltleletr  10726  elfz0ubfz0  13010  ssnn0fi  13352  caubnd  14713  sqreulem  14714  bezoutlem1  15880  pcprendvds  16170  prmreclem3  16247  ptcmpfi  22421  ufilen  22538  fcfnei  22643  bcthlem5  23935  aaliou  24937  wlkres  27463  wlkiswwlks2  27664  3cyclfrgrrn1  28073  n4cyclfrgr  28079  occon2  29074  occon3  29083  atexch  30167  sigaclci  31499  fisshasheq  32460  pfxwlk  32478  cusgr3cyclex  32491  frmin  33192  idinside  33653  exrecfnlem  34791  poimirlem32  35082  heibor1lem  35240  axc16g-o  36223  axc11-o  36240  aomclem2  39986  frege124d  40449  tratrb  41229  trsspwALT2  41512  leltletr  43837
  Copyright terms: Public domain W3C validator