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

Theorem syl9r 75
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 74 . 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:  sylan9r  687  ax12v2  2033  ax12vOLD  2034  ax12vOLDOLD  2035  nfimdOLD  2208  fununi  5860  dfimafn  6136  funimass3  6222  isomin  6461  oneqmin  6870  tz7.48lem  7396  fisupg  8066  fiinfg  8261  trcl  8460  coflim  8939  coftr  8951  axdc3lem2  9129  konigthlem  9242  indpi  9581  nnsub  10902  2ndc1stc  21002  kgencn2  21108  tx1stc  21201  filuni  21437  fclscf  21577  alexsubALTlem2  21600  alexsubALTlem3  21601  alexsubALT  21603  lpni  26484  dfimafnf  28619  dfon2lem6  30739  nodenselem8  30889  finixpnum  32363  heiborlem4  32582  lncvrelatN  33884  imbi13  37546  dfaimafn  39695
  Copyright terms: Public domain W3C validator