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  2493  rspc2vd  3911  trintss  5246  onfununi  8292  smoiun  8312  findcard2  9115  findcard2OLD  9235  findcard3  9236  findcard3OLD  9237  inficl  9368  en3lplem2  9556  infxpenlem  9956  alephordi  10017  cardaleph  10032  pwsdompw  10147  cfslb2n  10211  isf32lem10  10305  axdc4lem  10398  zorn2lem2  10440  alephreg  10525  inar1  10718  tskuni  10726  grudomon  10760  nqereu  10872  leltletr  11253  ltleletr  11255  elfz0ubfz0  13552  ssnn0fi  13897  caubnd  15250  sqreulem  15251  bezoutlem1  16427  rppwr  16447  pcprendvds  16719  prmreclem3  16797  ptcmpfi  23180  ufilen  23297  fcfnei  23402  bcthlem5  24708  aaliou  25714  wlkres  28660  wlkiswwlks2  28862  3cyclfrgrrn1  29271  n4cyclfrgr  29277  occon2  30272  occon3  30281  atexch  31365  sigaclci  32771  fisshasheq  33745  pfxwlk  33757  cusgr3cyclex  33770  idinside  34698  exrecfnlem  35879  poimirlem32  36139  heibor1lem  36297  axc16g-o  37425  axc11-o  37442  aomclem2  41411  frege124d  42107  tratrb  42892  trsspwALT2  43175
  Copyright terms: Public domain W3C validator