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  1838  ax12v2  2177  axprlem3  5431  fununi  6643  dfimafn  6971  funimass3  7074  isomin  7357  oneqmin  7820  tz7.48lem  8480  fisupg  9322  fiinfg  9537  trcl  9766  coflim  10299  coftr  10311  axdc3lem2  10489  konigthlem  10606  indpi  10945  nnsub  12308  2ndc1stc  23475  kgencn2  23581  tx1stc  23674  filuni  23909  fclscf  24049  alexsubALTlem2  24072  alexsubALTlem3  24073  alexsubALT  24075  nodenselem8  27751  n0subs  28375  lpni  30509  dfimafnf  32653  dfon2lem6  35770  bj-nnf-exlim  36739  finixpnum  37592  heiborlem4  37801  lncvrelatN  39764  imbi13  44518  dfaimafn  47115  sgoldbeven3prm  47708