Theorem sylan9 689

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  ax8  1996  ax9  2003  rspc2  3320  rspc3v  3325  trintssOLD  4770  copsexg  4956  chfnrn  6328  fvcofneq  6367  ffnfv  6388  f1elima  6520  onint  6995  peano5  7089  f1oweALT  7152  smoel2  7460  pssnn  8178  fiint  8237  dffi2  8329  alephnbtwn  8894  cfcof  9096  zorn2lem7  9324  suplem1pr  9874  addsrpr  9896  mulsrpr  9897  cau3lem  14094  divalglem8  15123  efgi  18132  elfrlmbasn0  20106  locfincmp  21329  tx1stc  21453  fbunfip  21673  filuni  21689  ufileu  21723  rescncf  22700  shmodsi  28248  spanuni  28403  spansneleq  28429  mdi  29154  dmdi  29161  dmdi4  29166  funimass4f  29437  bj-ax89  32667  wl-ax8clv1  33378  wl-ax8clv2  33381  poimirlem32  33441  ffnafv  41251