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  3505  rspc2  3587  rspc2v  3589  rspc3v  3594  rspc4v  3598  rspc8v  3600  copsexgw  5446  copsexg  5447  chfnrn  7003  fvcofneq  7047  ffnfv  7073  f1elima  7219  onint  7745  peano5  7845  f1oweALT  7926  smoel2  8305  pssnn  9105  php  9143  fiint  9239  dffi2  9338  alephnbtwn  9993  cfcof  10196  zorn2lem7  10424  suplem1pr  10975  addsrpr  10998  mulsrpr  10999  cau3lem  15290  divalglem8  16339  efgi  19660  elfrlmbasn0  21730  locfincmp  23482  tx1stc  23606  fbunfip  23825  filuni  23841  ufileu  23875  rescncf  24858  shmodsi  31477  spanuni  31632  spansneleq  31658  mdi  32383  dmdi  32390  dmdi4  32395  funimass4f  32727  tz9.1regs  35312  bj-ax89  36923  poimirlem32  37903  ffnafv  47531