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  2115  ax9  2123  spcimgft  3515  rspc2  3600  rspc2v  3602  rspc3v  3607  rspc4v  3611  rspc8v  3613  copsexgw  5453  copsexg  5454  chfnrn  7024  fvcofneq  7068  ffnfv  7094  f1elima  7241  onint  7769  peano5  7872  f1oweALT  7954  smoel2  8335  pssnn  9138  php  9177  fiint  9284  fiintOLD  9285  dffi2  9381  alephnbtwn  10031  cfcof  10234  zorn2lem7  10462  suplem1pr  11012  addsrpr  11035  mulsrpr  11036  cau3lem  15328  divalglem8  16377  efgi  19656  elfrlmbasn0  21679  locfincmp  23420  tx1stc  23544  fbunfip  23763  filuni  23779  ufileu  23813  rescncf  24797  shmodsi  31325  spanuni  31480  spansneleq  31506  mdi  32231  dmdi  32238  dmdi4  32243  funimass4f  32568  bj-ax89  36673  poimirlem32  37653  ffnafv  47176