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  1839  ax12v2  2180  fununi  6653  dfimafn  6984  funimass3  7087  isomin  7373  oneqmin  7836  tz7.48lem  8497  fisupg  9352  fiinfg  9568  trcl  9797  coflim  10330  coftr  10342  axdc3lem2  10520  konigthlem  10637  indpi  10976  nnsub  12337  2ndc1stc  23480  kgencn2  23586  tx1stc  23679  filuni  23914  fclscf  24054  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALT  24080  nodenselem8  27754  n0subs  28378  lpni  30512  dfimafnf  32655  dfon2lem6  35752  bj-nnf-exlim  36722  finixpnum  37565  heiborlem4  37774  lncvrelatN  39738  imbi13  44491  dfaimafn  47080  sgoldbeven3prm  47657