Theorem sylan9 688

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  1998  ax9  2005  rspc2  3310  rspc3v  3314  trintssOLD  4735  copsexg  4921  chfnrn  6285  fvcofneq  6324  ffnfv  6344  f1elima  6475  onint  6943  peano5  7037  f1oweALT  7100  smoel2  7406  pssnn  8123  fiint  8182  dffi2  8274  alephnbtwn  8839  cfcof  9041  zorn2lem7  9269  suplem1pr  9819  addsrpr  9841  mulsrpr  9842  cau3lem  14023  divalglem8  15042  efgi  18048  elfrlmbasn0  20020  locfincmp  21234  tx1stc  21358  fbunfip  21578  filuni  21594  ufileu  21628  rescncf  22603  shmodsi  28088  spanuni  28243  spansneleq  28269  mdi  28994  dmdi  29001  dmdi4  29006  funimass4f  29271  bj-ax89  32301  poimirlem32  33059  ffnafv  40542