Theorem sylan9 650

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
sylan9.1	|- ( ph -> ( ps -> ch ) )
sylan9.2	|- ( th -> ( ch -> ta ) )

Assertion

Ref	Expression
sylan9	|- ( ( ph /\ th ) -> ( ps -> ta ) )

Proof of Theorem sylan9

Step	Hyp	Ref	Expression
1		sylan9.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		sylan9.2	. . 3 |- ( th -> ( ch -> ta ) )
3	1, 2	syl9 71	. 2 |- ( ph -> ( th -> ( ps -> ta ) ) )
4	3	imp 429	1 |- ( ( ph /\ th ) -> ( ps -> ta ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  sbal1OLD  2174  rspc2  3067  rspc3v  3071  trintss  4389  copsexg  4564  copsexgOLD  4565  chfnrn  5802  fvcofneq  5839  ffnfv  5856  f1elima  5963  onint  6395  peano5  6488  f1oweALT  6550  smoel2  6810  th3q  7197  pssnn  7519  fiint  7576  dffi2  7661  alephnbtwn  8229  cfcof  8431  zorn2lem7  8659  suplem1pr  9208  cau3lem  12825  divalglem8  13586  efgi  16195  elfrlmbasn0  18031  tx1stc  19064  fbunfip  19283  filuni  19299  ufileu  19333  rescncf  20314  shmodsi  24614  spanuni  24769  spansneleq  24795  mdi  25521  dmdi  25528  dmdi4  25533  funimass4f  25774  locfincmp  28417  ffnafv  29920