Theorem sylan9 516

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 411	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  ax8  2149  ax9  2157  spcimgft  3515  rspc2  3590  rspc2v  3592  rspc3v  3597  rspc4v  3601  rspc8v  3603  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  chfnrn  7044  fvcofneq  7088  ffnfv  7114  f1elima  7261  onint  7785  peano5  7886  f1oweALT  7965  smoel2  8346  pssnn  9149  php  9187  fiint  9282  dffi2  9379  alephnbtwn  10051  cfcof  10253  zorn2lem7  10481  suplem1pr  11032  addsrpr  11055  mulsrpr  11056  cau3lem  15402  divalglem8  16453  efgi  19784  elfrlmbasn0  21913  locfincmp  23683  tx1stc  23807  fbunfip  24026  filuni  24042  ufileu  24076  rescncf  25056  shmodsi  31741  spanuni  31896  spansneleq  31922  mdi  32647  dmdi  32654  dmdi4  32659  funimass4f  32982  tz9.1regs  35547  bj-ax89  37301  poimirlem32  38303  ffnafv  47908