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  3525  rspc2  3610  rspc2v  3612  rspc3v  3617  rspc4v  3621  rspc8v  3623  copsexgw  5465  copsexg  5466  chfnrn  7039  fvcofneq  7083  ffnfv  7109  f1elima  7256  onint  7784  peano5  7889  f1oweALT  7971  smoel2  8377  pssnn  9182  php  9221  fiint  9338  fiintOLD  9339  dffi2  9435  alephnbtwn  10085  cfcof  10288  zorn2lem7  10516  suplem1pr  11066  addsrpr  11089  mulsrpr  11090  cau3lem  15373  divalglem8  16419  efgi  19700  elfrlmbasn0  21723  locfincmp  23464  tx1stc  23588  fbunfip  23807  filuni  23823  ufileu  23857  rescncf  24841  shmodsi  31370  spanuni  31525  spansneleq  31551  mdi  32276  dmdi  32283  dmdi4  32288  funimass4f  32615  bj-ax89  36696  poimirlem32  37676  ffnafv  47200