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  2155  ax9  2163  spcimgft  3523  rspc2  3599  rspc2v  3601  rspc3v  3606  rspc4v  3610  rspc8v  3612  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  chfnrn  7045  fvcofneq  7089  ffnfv  7115  f1elima  7262  onint  7788  peano5  7889  f1oweALT  7968  smoel2  8349  pssnn  9152  php  9190  fiint  9285  dffi2  9382  alephnbtwn  10054  cfcof  10257  zorn2lem7  10485  suplem1pr  11036  addsrpr  11059  mulsrpr  11060  cau3lem  15405  divalglem8  16457  efgi  19788  elfrlmbasn0  21881  locfincmp  23651  tx1stc  23775  fbunfip  23994  filuni  24010  ufileu  24044  rescncf  25024  shmodsi  31681  spanuni  31836  spansneleq  31862  mdi  32587  dmdi  32594  dmdi4  32599  funimass4f  32922  tz9.1regs  35469  bj-ax89  37189  poimirlem32  38190  ffnafv  47796