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  2114  ax9  2122  spcimgft  3546  rspc2  3631  rspc2v  3633  rspc3v  3638  rspc4v  3642  rspc8v  3644  copsexgw  5495  copsexg  5496  chfnrn  7069  fvcofneq  7113  ffnfv  7139  f1elima  7283  onint  7810  peano5  7915  f1oweALT  7997  smoel2  8403  pssnn  9208  php  9247  fiint  9366  fiintOLD  9367  dffi2  9463  alephnbtwn  10111  cfcof  10314  zorn2lem7  10542  suplem1pr  11092  addsrpr  11115  mulsrpr  11116  cau3lem  15393  divalglem8  16437  efgi  19737  elfrlmbasn0  21783  locfincmp  23534  tx1stc  23658  fbunfip  23877  filuni  23893  ufileu  23927  rescncf  24923  shmodsi  31408  spanuni  31563  spansneleq  31589  mdi  32314  dmdi  32321  dmdi4  32326  funimass4f  32647  bj-ax89  36679  poimirlem32  37659  ffnafv  47183