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  1842  ax12v2  2184  axprlem3  5367  fununi  6564  dfimafn  6893  funimass3  6996  isomin  7280  oneqmin  7742  tz7.48lem  8369  fisupg  9183  fiinfg  9396  trcl  9629  coflim  10163  coftr  10175  axdc3lem2  10353  konigthlem  10470  indpi  10809  nnsub  12180  2ndc1stc  23386  kgencn2  23492  tx1stc  23585  filuni  23820  fclscf  23960  alexsubALTlem2  23983  alexsubALTlem3  23984  alexsubALT  23986  nodenselem8  27650  n0subs  28309  lpni  30481  dfimafnf  32640  r1omhfb  35195  r1omhfbregs  35205  dfon2lem6  35902  bj-nnf-exlim  36873  finixpnum  37718  heiborlem4  37927  lncvrelatN  39953  imbi13  44677  relpmin  45109  dfaimafn  47327  sgoldbeven3prm  47945