Theorem sylan9 510

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 409	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ax8  2120  ax9  2128  rspc2  3633  rspc2v  3635  rspc3v  3638  copsexgw  5383  copsexg  5384  chfnrn  6821  fvcofneq  6861  ffnfv  6884  f1elima  7023  onint  7512  peano5  7607  f1oweALT  7675  smoel2  8002  pssnn  8738  fiint  8797  dffi2  8889  alephnbtwn  9499  cfcof  9698  zorn2lem7  9926  suplem1pr  10476  addsrpr  10499  mulsrpr  10500  cau3lem  14716  divalglem8  15753  efgi  18847  elfrlmbasn0  20909  locfincmp  22136  tx1stc  22260  fbunfip  22479  filuni  22495  ufileu  22529  rescncf  23507  shmodsi  29168  spanuni  29323  spansneleq  29349  mdi  30074  dmdi  30081  dmdi4  30086  funimass4f  30384  bj-ax89  34013  poimirlem32  34926  ffnafv  43377