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  512  19.38b  1842  ax12v2  2177  fununi  6415  dfimafn  6721  funimass3  6820  isomin  7090  oneqmin  7525  tz7.48lem  8093  fisupg  8812  fiinfg  9009  trcl  9216  coflim  9734  coftr  9746  axdc3lem2  9924  konigthlem  10041  indpi  10380  nnsub  11731  2ndc1stc  22165  kgencn2  22271  tx1stc  22364  filuni  22599  fclscf  22739  alexsubALTlem2  22762  alexsubALTlem3  22763  alexsubALT  22765  lpni  28376  dfimafnf  30507  dfon2lem6  33293  nodenselem8  33492  bj-nnf-exlim  34516  finixpnum  35357  heiborlem4  35567  lncvrelatN  37392  imbi13  41644  dfaimafn  44148  sgoldbeven3prm  44727
 Copyright terms: Public domain W3C validator