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  axc16gALT  2458  trintss  4929  onfununi  7642  smoiun  7662  findcard2  8407  findcard3  8410  inficl  8538  en3lplem2  8723  r1sdom  8852  infxpenlem  9087  alephordi  9148  cardaleph  9163  pwsdompw  9279  cfslb2n  9343  isf32lem10  9437  axdc4lem  9530  zorn2lem2  9572  alephreg  9657  inar1  9850  tskuni  9858  grudomon  9892  nqereu  10004  ltleletr  10384  elfz0ubfz0  12651  ssnn0fi  12992  caubnd  14383  sqreulem  14384  bezoutlem1  15537  pcprendvds  15824  prmreclem3  15901  ptcmpfi  21896  ufilen  22013  fcfnei  22118  bcthlem5  23405  aaliou  24384  wlkres  26859  wlkiswwlks2  27066  rspc2vd  27545  3cyclfrgrrn1  27565  n4cyclfrgr  27571  occon2  28603  occon3  28612  atexch  29696  sigaclci  30642  frmin  32186  idinside  32635  poimirlem32  33865  heibor1lem  34030  axc16g-o  34890  axc11-o  34907  aomclem2  38302  frege124d  38728  tratrb  39414  trsspwALT2  39707  leltletr  42043
  Copyright terms: Public domain W3C validator