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  2119  ax9  2127  spcimgft  3501  rspc2  3583  rspc2v  3585  rspc3v  3590  rspc4v  3594  rspc8v  3596  copsexgw  5436  copsexg  5437  chfnrn  6992  fvcofneq  7036  ffnfv  7062  f1elima  7207  onint  7733  peano5  7833  f1oweALT  7914  smoel2  8293  pssnn  9091  php  9129  fiint  9225  dffi2  9324  alephnbtwn  9979  cfcof  10182  zorn2lem7  10410  suplem1pr  10961  addsrpr  10984  mulsrpr  10985  cau3lem  15276  divalglem8  16325  efgi  19646  elfrlmbasn0  21716  locfincmp  23468  tx1stc  23592  fbunfip  23811  filuni  23827  ufileu  23861  rescncf  24844  shmodsi  31413  spanuni  31568  spansneleq  31594  mdi  32319  dmdi  32326  dmdi4  32331  funimass4f  32664  tz9.1regs  35239  bj-ax89  36822  poimirlem32  37792  ffnafv  47359