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  510  19.38b  1844  ax12v2  2174  fununi  6624  dfimafn  6955  funimass3  7056  isomin  7334  oneqmin  7788  tz7.48lem  8441  fisupg  9291  fiinfg  9494  trcl  9723  coflim  10256  coftr  10268  axdc3lem2  10446  konigthlem  10563  indpi  10902  nnsub  12256  2ndc1stc  22955  kgencn2  23061  tx1stc  23154  filuni  23389  fclscf  23529  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALT  23555  nodenselem8  27194  lpni  29733  dfimafnf  31860  dfon2lem6  34760  bj-nnf-exlim  35634  finixpnum  36473  heiborlem4  36682  lncvrelatN  38652  imbi13  43281  dfaimafn  45873  sgoldbeven3prm  46451