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  3501  rspc2  3586  rspc2v  3588  rspc3v  3593  rspc4v  3597  rspc8v  3599  copsexgw  5433  copsexg  5434  chfnrn  6983  fvcofneq  7027  ffnfv  7053  f1elima  7200  onint  7726  peano5  7826  f1oweALT  7907  smoel2  8286  pssnn  9082  php  9121  fiint  9216  fiintOLD  9217  dffi2  9313  alephnbtwn  9965  cfcof  10168  zorn2lem7  10396  suplem1pr  10946  addsrpr  10969  mulsrpr  10970  cau3lem  15262  divalglem8  16311  efgi  19598  elfrlmbasn0  21670  locfincmp  23411  tx1stc  23535  fbunfip  23754  filuni  23770  ufileu  23804  rescncf  24788  shmodsi  31333  spanuni  31488  spansneleq  31514  mdi  32239  dmdi  32246  dmdi4  32251  funimass4f  32580  tz9.1regs  35067  bj-ax89  36652  poimirlem32  37632  ffnafv  47155