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  3509  rspc2  3594  rspc2v  3596  rspc3v  3601  rspc4v  3605  rspc8v  3607  copsexgw  5445  copsexg  5446  chfnrn  7003  fvcofneq  7047  ffnfv  7073  f1elima  7220  onint  7746  peano5  7849  f1oweALT  7930  smoel2  8309  pssnn  9109  php  9148  fiint  9253  fiintOLD  9254  dffi2  9350  alephnbtwn  10000  cfcof  10203  zorn2lem7  10431  suplem1pr  10981  addsrpr  11004  mulsrpr  11005  cau3lem  15297  divalglem8  16346  efgi  19625  elfrlmbasn0  21648  locfincmp  23389  tx1stc  23513  fbunfip  23732  filuni  23748  ufileu  23782  rescncf  24766  shmodsi  31291  spanuni  31446  spansneleq  31472  mdi  32197  dmdi  32204  dmdi4  32209  funimass4f  32534  bj-ax89  36639  poimirlem32  37619  ffnafv  47145