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  511  19.38b  1837  ax12v2  2175  fununi  6423  dfimafn  6722  funimass3  6818  isomin  7084  oneqmin  7514  tz7.48lem  8071  fisupg  8760  fiinfg  8957  trcl  9164  coflim  9677  coftr  9689  axdc3lem2  9867  konigthlem  9984  indpi  10323  nnsub  11675  2ndc1stc  22053  kgencn2  22159  tx1stc  22252  filuni  22487  fclscf  22627  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALT  22653  lpni  28251  dfimafnf  30375  dfon2lem6  33028  nodenselem8  33190  bj-nnf-exlim  34080  finixpnum  34871  heiborlem4  35086  lncvrelatN  36911  imbi13  40847  dfaimafn  43358  sgoldbeven3prm  43942