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 206  df-an 396

This theorem is referenced by:  ax8  2114  ax9  2122  rspc2  3560  rspc2v  3562  rspc3v  3565  copsexgw  5398  copsexg  5399  chfnrn  6908  fvcofneq  6951  ffnfv  6974  f1elima  7117  onint  7617  peano5  7714  peano5OLD  7715  f1oweALT  7788  smoel2  8165  pssnn  8913  pssnnOLD  8969  fiint  9021  dffi2  9112  alephnbtwn  9758  cfcof  9961  zorn2lem7  10189  suplem1pr  10739  addsrpr  10762  mulsrpr  10763  cau3lem  14994  divalglem8  16037  efgi  19240  elfrlmbasn0  20880  locfincmp  22585  tx1stc  22709  fbunfip  22928  filuni  22944  ufileu  22978  rescncf  23966  shmodsi  29652  spanuni  29807  spansneleq  29833  mdi  30558  dmdi  30565  dmdi4  30570  funimass4f  30873  bj-ax89  34786  poimirlem32  35736  ffnafv  44550