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  6428  dfimafn  6727  funimass3  6823  isomin  7089  oneqmin  7519  tz7.48lem  8076  fisupg  8765  fiinfg  8962  trcl  9169  coflim  9682  coftr  9694  axdc3lem2  9872  konigthlem  9989  indpi  10328  nnsub  11680  2ndc1stc  22058  kgencn2  22164  tx1stc  22257  filuni  22492  fclscf  22632  alexsubALTlem2  22655  alexsubALTlem3  22656  alexsubALT  22658  lpni  28256  dfimafnf  30380  dfon2lem6  33033  nodenselem8  33195  bj-nnf-exlim  34085  finixpnum  34876  heiborlem4  35091  lncvrelatN  36916  imbi13  40852  dfaimafn  43363  sgoldbeven3prm  43947