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  1868  ax12v2  2221  axprlem3  5399  fununi  6614  dfimafn  6946  funimass3  7052  isomin  7338  oneqmin  7801  tz7.48lem  8430  fisupg  9250  fiinfg  9463  trcl  9699  coflim  10247  coftr  10259  axdc3lem2  10437  konigthlem  10555  indpi  10894  nnsub  12282  2ndc1stc  23579  kgencn2  23685  tx1stc  23778  filuni  24013  fclscf  24153  alexsubALTlem2  24176  alexsubALTlem3  24177  alexsubALT  24179  nodenselem8  27823  n0subs  28524  lpni  30775  dfimafnf  32924  r1omhfb  35451  r1omhfbregs  35485  dfon2lem6  36213  bj-nnf-exlim  37310  finixpnum  38181  heiborlem4  38390  lncvrelatN  40482  imbi13  45158  relpmin  45590  dfaimafn  47828  sgoldbeven3prm  48474