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  512  19.38b  1842  ax12v2  2177  fununi  6399  dfimafn  6703  funimass3  6801  isomin  7069  oneqmin  7500  tz7.48lem  8060  fisupg  8750  fiinfg  8947  trcl  9154  coflim  9672  coftr  9684  axdc3lem2  9862  konigthlem  9979  indpi  10318  nnsub  11669  2ndc1stc  22056  kgencn2  22162  tx1stc  22255  filuni  22490  fclscf  22630  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALT  22656  lpni  28263  dfimafnf  30395  dfon2lem6  33146  nodenselem8  33308  bj-nnf-exlim  34200  finixpnum  35042  heiborlem4  35252  lncvrelatN  37077  imbi13  41226  dfaimafn  43721  sgoldbeven3prm  44301