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  1843  ax12v2  2173  fununi  6576  dfimafn  6905  funimass3  7004  isomin  7281  oneqmin  7734  tz7.48lem  8386  fisupg  9234  fiinfg  9434  trcl  9663  coflim  10196  coftr  10208  axdc3lem2  10386  konigthlem  10503  indpi  10842  nnsub  12196  2ndc1stc  22800  kgencn2  22906  tx1stc  22999  filuni  23234  fclscf  23374  alexsubALTlem2  23397  alexsubALTlem3  23398  alexsubALT  23400  nodenselem8  27037  lpni  29369  dfimafnf  31497  dfon2lem6  34303  bj-nnf-exlim  35211  finixpnum  36053  heiborlem4  36263  lncvrelatN  38234  imbi13  42783  dfaimafn  45368  sgoldbeven3prm  45946
  Copyright terms: Public domain W3C validator