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  expt  177  sylan9r  516  19.38b  1860  ax12v2  2213  axprlem3  5379  fununi  6591  dfimafn  6924  funimass3  7030  isomin  7316  oneqmin  7778  tz7.48lem  8406  fisupg  9226  fiinfg  9441  trcl  9677  coflim  10212  coftr  10224  axdc3lem2  10402  konigthlem  10520  indpi  10859  nnsub  12251  2ndc1stc  23499  kgencn2  23605  tx1stc  23698  filuni  23933  fclscf  24073  alexsubALTlem2  24096  alexsubALTlem3  24097  alexsubALT  24099  nodenselem8  27743  n0subs  28444  lpni  30640  dfimafnf  32799  r1omhfb  35369  r1omhfbregs  35394  dfon2lem6  36097  bj-nnf-exlim  37196  finixpnum  38065  heiborlem4  38274  lncvrelatN  40366  imbi13  45057  relpmin  45489  dfaimafn  47720  sgoldbeven3prm  48366