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  2117  ax9  2125  spcimgft  3499  rspc2  3581  rspc2v  3583  rspc3v  3588  rspc4v  3592  rspc8v  3594  copsexgw  5425  copsexg  5426  chfnrn  6977  fvcofneq  7021  ffnfv  7047  f1elima  7192  onint  7718  peano5  7818  f1oweALT  7899  smoel2  8278  pssnn  9073  php  9111  fiint  9206  dffi2  9302  alephnbtwn  9957  cfcof  10160  zorn2lem7  10388  suplem1pr  10938  addsrpr  10961  mulsrpr  10962  cau3lem  15257  divalglem8  16306  efgi  19626  elfrlmbasn0  21695  locfincmp  23436  tx1stc  23560  fbunfip  23779  filuni  23795  ufileu  23829  rescncf  24812  shmodsi  31361  spanuni  31516  spansneleq  31542  mdi  32267  dmdi  32274  dmdi4  32279  funimass4f  32611  tz9.1regs  35122  bj-ax89  36712  poimirlem32  37692  ffnafv  47202