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

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9r.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 77	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	com12 32	1 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))

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  508  19.38b  1843  ax12v2  2187  axprlem3  5362  fununi  6567  dfimafn  6896  funimass3  7000  isomin  7285  oneqmin  7747  tz7.48lem  8373  fisupg  9191  fiinfg  9407  trcl  9640  coflim  10174  coftr  10186  axdc3lem2  10364  konigthlem  10482  indpi  10821  nnsub  12212  2ndc1stc  23426  kgencn2  23532  tx1stc  23625  filuni  23860  fclscf  24000  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALT  24026  nodenselem8  27669  n0subs  28369  lpni  30566  dfimafnf  32724  r1omhfb  35272  r1omhfbregs  35297  dfon2lem6  35984  bj-nnf-exlim  37073  finixpnum  37940  heiborlem4  38149  lncvrelatN  40241  imbi13  44965  relpmin  45397  dfaimafn  47625  sgoldbeven3prm  48271