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

Theorem syl9r 78
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
syl9r.1 (𝜑 → (𝜓𝜒))
syl9r.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
syl9r (𝜃 → (𝜑 → (𝜓𝜏)))

Proof of Theorem syl9r
StepHypRef Expression
1 syl9r.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl9r.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2syl9 77 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43com12 32 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:  peirceroll  85  imim12  105  sylan9r  509  19.38b  1832  ax12v2  2169  fununi  6423  dfimafn  6722  funimass3  6817  isomin  7079  oneqmin  7508  tz7.48lem  8068  fisupg  8755  fiinfg  8952  trcl  9159  coflim  9672  coftr  9684  axdc3lem2  9862  konigthlem  9979  indpi  10318  nnsub  11670  2ndc1stc  21989  kgencn2  22095  tx1stc  22188  filuni  22423  fclscf  22563  alexsubALTlem2  22586  alexsubALTlem3  22587  alexsubALT  22589  lpni  28185  dfimafnf  30310  dfon2lem6  32931  nodenselem8  33093  bj-nnf-exlim  33983  finixpnum  34759  heiborlem4  34975  lncvrelatN  36799  imbi13  40734  dfaimafn  43245  sgoldbeven3prm  43795
  Copyright terms: Public domain W3C validator