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:  sylan9r  691  ax12v2  2089  nfimdOLD  2262  fununi  6002  dfimafn  6284  funimass3  6373  isomin  6627  oneqmin  7047  tz7.48lem  7581  fisupg  8249  fiinfg  8446  trcl  8642  coflim  9121  coftr  9133  axdc3lem2  9311  konigthlem  9428  indpi  9767  nnsub  11097  2ndc1stc  21302  kgencn2  21408  tx1stc  21501  filuni  21736  fclscf  21876  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALT  21902  lpni  27462  dfimafnf  29564  dfon2lem6  31817  nodenselem8  31966  finixpnum  33524  heiborlem4  33743  lncvrelatN  35385  imbi13  39043  dfaimafn  41566  sgoldbeven3prm  41996
  Copyright terms: Public domain W3C validator