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  2112  ax9  2120  spcimgft  3546  rspc2  3631  rspc2v  3633  rspc3v  3638  rspc4v  3642  rspc8v  3644  copsexgw  5501  copsexg  5502  chfnrn  7069  fvcofneq  7113  ffnfv  7139  f1elima  7283  onint  7810  peano5  7916  f1oweALT  7996  smoel2  8402  pssnn  9207  php  9245  fiint  9364  fiintOLD  9365  dffi2  9461  alephnbtwn  10109  cfcof  10312  zorn2lem7  10540  suplem1pr  11090  addsrpr  11113  mulsrpr  11114  cau3lem  15390  divalglem8  16434  efgi  19752  elfrlmbasn0  21801  locfincmp  23550  tx1stc  23674  fbunfip  23893  filuni  23909  ufileu  23943  rescncf  24937  shmodsi  31418  spanuni  31573  spansneleq  31599  mdi  32324  dmdi  32331  dmdi4  32336  funimass4f  32654  bj-ax89  36661  poimirlem32  37639  ffnafv  47121