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  29764  dfimafnf  31891  dfon2lem6  34791  bj-nnf-exlim  35682  finixpnum  36521  heiborlem4  36730  lncvrelatN  38700  imbi13  43329  dfaimafn  45921  sgoldbeven3prm  46499