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

Theorem syl9r 76
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 75 . 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  688  ax12v2  2036  ax12vOLD  2037  ax12vOLDOLD  2038  nfimdOLD  2214  fununi  5878  dfimafn  6155  funimass3  6241  isomin  6487  oneqmin  6897  tz7.48lem  7423  fisupg  8093  fiinfg  8288  trcl  8487  coflim  8966  coftr  8978  axdc3lem2  9156  konigthlem  9269  indpi  9608  nnsub  10936  2ndc1stc  21064  kgencn2  21170  tx1stc  21263  filuni  21499  fclscf  21639  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALT  21665  lpni  26722  dfimafnf  28817  dfon2lem6  30937  nodenselem8  31087  finixpnum  32564  heiborlem4  32783  lncvrelatN  34085  imbi13  37747  dfaimafn  39894
  Copyright terms: Public domain W3C validator