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  1834  ax12v2  2171  fununi  6426  dfimafn  6725  funimass3  6820  isomin  7082  oneqmin  7508  tz7.48lem  8068  fisupg  8755  fiinfg  8952  trcl  9159  coflim  9672  coftr  9684  axdc3lem2  9862  konigthlem  9979  indpi  10318  nnsub  11670  2ndc1stc  21975  kgencn2  22081  tx1stc  22174  filuni  22409  fclscf  22549  alexsubALTlem2  22572  alexsubALTlem3  22573  alexsubALT  22575  lpni  28171  dfimafnf  30296  dfon2lem6  32917  nodenselem8  33079  bj-nnf-exlim  33969  finixpnum  34744  heiborlem4  34960  lncvrelatN  36784  imbi13  40719  dfaimafn  43230  sgoldbeven3prm  43780
  Copyright terms: Public domain W3C validator