Theorem syl9r 79

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 78	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	com12 33	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  86  imim12  106  expt  178  sylan9r  517  19.38b  1871  ax12v2  2215  axprlem3  5398  fununi  6613  dfimafn  6945  funimass3  7051  isomin  7337  oneqmin  7800  tz7.48lem  8429  fisupg  9249  fiinfg  9462  trcl  9698  coflim  10246  coftr  10258  axdc3lem2  10436  konigthlem  10554  indpi  10893  nnsub  12281  2ndc1stc  23589  kgencn2  23695  tx1stc  23788  filuni  24023  fclscf  24163  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALT  24189  nodenselem8  27836  n0subs  28537  lpni  30813  dfimafnf  32962  r1omhfb  35489  r1omhfbregs  35531  dfon2lem6  36259  bj-nnf-exlim  37366  finixpnum  38237  heiborlem4  38446  lncvrelatN  40536  imbi13  45212  relpmin  45644  dfaimafn  47885  sgoldbeven3prm  48531