Theorem sylan9 517

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylan9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
sylan9	⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 78	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 412	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ax8  2152  ax9  2160  spcimgft  3517  rspc2  3592  rspc2v  3594  rspc3v  3599  rspc4v  3603  rspc8v  3605  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  chfnrn  7048  fvcofneq  7092  ffnfv  7118  f1elima  7266  onint  7795  peano5  7896  f1oweALT  7975  smoel2  8356  pssnn  9160  php  9198  fiint  9293  dffi2  9390  alephnbtwn  10071  cfcof  10273  zorn2lem7  10501  suplem1pr  11052  addsrpr  11075  mulsrpr  11076  cau3lem  15430  divalglem8  16480  efgi  19833  elfrlmbasn0  21963  locfincmp  23734  tx1stc  23858  fbunfip  24077  filuni  24093  ufileu  24127  rescncf  25107  shmodsi  31812  spanuni  31967  spansneleq  31993  mdi  32718  dmdi  32725  dmdi4  32730  funimass4f  33053  tz9.1regs  35604  bj-ax89  37358  poimirlem32  38360  ffnafv  47966