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  1846  ax12v2  2176  fununi  6505  dfimafn  6826  funimass3  6925  isomin  7201  oneqmin  7640  tz7.48lem  8256  fisupg  9023  fiinfg  9219  trcl  9469  coflim  10001  coftr  10013  axdc3lem2  10191  konigthlem  10308  indpi  10647  nnsub  12000  2ndc1stc  22583  kgencn2  22689  tx1stc  22782  filuni  23017  fclscf  23157  alexsubALTlem2  23180  alexsubALTlem3  23181  alexsubALT  23183  lpni  28821  dfimafnf  30950  dfon2lem6  33743  nodenselem8  33873  bj-nnf-exlim  34917  finixpnum  35741  heiborlem4  35951  lncvrelatN  37774  imbi13  42093  dfaimafn  44608  sgoldbeven3prm  45187