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  2115  ax9  2123  spcimgft  3512  rspc2  3597  rspc2v  3599  rspc3v  3604  rspc4v  3608  rspc8v  3610  copsexgw  5450  copsexg  5451  chfnrn  7021  fvcofneq  7065  ffnfv  7091  f1elima  7238  onint  7766  peano5  7869  f1oweALT  7951  smoel2  8332  pssnn  9132  php  9171  fiint  9277  fiintOLD  9278  dffi2  9374  alephnbtwn  10024  cfcof  10227  zorn2lem7  10455  suplem1pr  11005  addsrpr  11028  mulsrpr  11029  cau3lem  15321  divalglem8  16370  efgi  19649  elfrlmbasn0  21672  locfincmp  23413  tx1stc  23537  fbunfip  23756  filuni  23772  ufileu  23806  rescncf  24790  shmodsi  31318  spanuni  31473  spansneleq  31499  mdi  32224  dmdi  32231  dmdi4  32236  funimass4f  32561  bj-ax89  36666  poimirlem32  37646  ffnafv  47172