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  2120  ax9  2128  spcimgft  3492  rspc2  3574  rspc2v  3576  rspc3v  3581  rspc4v  3585  rspc8v  3587  copsexgw  5439  copsexg  5440  chfnrn  6996  fvcofneq  7040  ffnfv  7066  f1elima  7212  onint  7738  peano5  7838  f1oweALT  7919  smoel2  8297  pssnn  9097  php  9135  fiint  9231  dffi2  9330  alephnbtwn  9987  cfcof  10190  zorn2lem7  10418  suplem1pr  10969  addsrpr  10992  mulsrpr  10993  cau3lem  15311  divalglem8  16363  efgi  19688  elfrlmbasn0  21756  locfincmp  23504  tx1stc  23628  fbunfip  23847  filuni  23863  ufileu  23897  rescncf  24877  shmodsi  31478  spanuni  31633  spansneleq  31659  mdi  32384  dmdi  32391  dmdi4  32396  funimass4f  32728  tz9.1regs  35297  bj-ax89  36992  poimirlem32  37990  ffnafv  47634