Theorem sylan9 512

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 407	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ax8  2125  ax9  2133  spcimgft  3492  rspc2  3569  rspc2v  3571  rspc3v  3576  rspc4v  3580  rspc8v  3582  copsexgw  5430  copsexgwOLD  5431  copsexg  5432  chfnrn  6990  fvcofneq  7034  ffnfv  7060  f1elima  7207  onint  7733  peano5  7833  f1oweALT  7914  smoel2  8293  pssnn  9093  php  9131  fiint  9227  dffi2  9326  alephnbtwn  9984  cfcof  10187  zorn2lem7  10415  suplem1pr  10966  addsrpr  10989  mulsrpr  10990  cau3lem  15308  divalglem8  16360  efgi  19685  elfrlmbasn0  21738  locfincmp  23509  tx1stc  23633  fbunfip  23852  filuni  23868  ufileu  23902  rescncf  24882  shmodsi  31478  spanuni  31633  spansneleq  31659  mdi  32384  dmdi  32391  dmdi4  32396  funimass4f  32729  tz9.1regs  35315  bj-ax89  37019  poimirlem32  38019  ffnafv  47634