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  2186  axprlem3  5370  fununi  6567  dfimafn  6896  funimass3  6999  isomin  7283  oneqmin  7745  tz7.48lem  8372  fisupg  9188  fiinfg  9404  trcl  9637  coflim  10171  coftr  10183  axdc3lem2  10361  konigthlem  10479  indpi  10818  nnsub  12189  2ndc1stc  23395  kgencn2  23501  tx1stc  23594  filuni  23829  fclscf  23969  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALT  23995  nodenselem8  27659  n0subs  28359  lpni  30555  dfimafnf  32714  r1omhfb  35268  r1omhfbregs  35293  dfon2lem6  35980  bj-nnf-exlim  36957  finixpnum  37806  heiborlem4  38015  lncvrelatN  40041  imbi13  44761  relpmin  45193  dfaimafn  47411  sgoldbeven3prm  48029