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  508  19.38b  1841  ax12v2  2180  axprlem3  5383  fununi  6594  dfimafn  6926  funimass3  7029  isomin  7315  oneqmin  7779  tz7.48lem  8412  fisupg  9242  fiinfg  9459  trcl  9688  coflim  10221  coftr  10233  axdc3lem2  10411  konigthlem  10528  indpi  10867  nnsub  12237  2ndc1stc  23345  kgencn2  23451  tx1stc  23544  filuni  23779  fclscf  23919  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALT  23945  nodenselem8  27610  n0subs  28260  lpni  30416  dfimafnf  32567  dfon2lem6  35783  bj-nnf-exlim  36751  finixpnum  37606  heiborlem4  37815  lncvrelatN  39782  imbi13  44517  relpmin  44949  dfaimafn  47170  sgoldbeven3prm  47788