Theorem sylan9 507

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 77	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	imp 406	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ax8  2114  ax9  2122  spcimgft  3558  rspc2  3644  rspc2v  3646  rspc3v  3651  rspc4v  3655  rspc8v  3657  copsexgw  5510  copsexg  5511  chfnrn  7082  fvcofneq  7127  ffnfv  7153  f1elima  7300  onint  7826  peano5  7932  peano5OLD  7933  f1oweALT  8013  smoel2  8419  pssnn  9234  php  9273  fiint  9394  fiintOLD  9395  dffi2  9492  alephnbtwn  10140  cfcof  10343  zorn2lem7  10571  suplem1pr  11121  addsrpr  11144  mulsrpr  11145  cau3lem  15403  divalglem8  16448  efgi  19761  elfrlmbasn0  21806  locfincmp  23555  tx1stc  23679  fbunfip  23898  filuni  23914  ufileu  23948  rescncf  24942  shmodsi  31421  spanuni  31576  spansneleq  31602  mdi  32327  dmdi  32334  dmdi4  32339  funimass4f  32656  bj-ax89  36644  poimirlem32  37612  ffnafv  47086