Theorem sylan9 655

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	|- ( 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 70	. 2 |- ( ph -> ( th -> ( ps -> ta ) ) )
4	3	imp 427	1 |- ( ( ph /\ th ) -> ( ps -> ta ) )

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  rspc2  3167  rspc3v  3171  trintss  4504  copsexg  4675  chfnrn  5975  fvcofneq  6016  ffnfv  6035  f1elima  6151  onint  6612  peano5  6706  f1oweALT  6767  smoel2  7066  pssnn  7772  fiint  7830  dffi2  7916  alephnbtwn  8483  cfcof  8685  zorn2lem7  8913  suplem1pr  9459  addsrpr  9481  mulsrpr  9482  cau3lem  13334  divalglem8  14265  efgi  17059  elfrlmbasn0  19090  locfincmp  20317  tx1stc  20441  fbunfip  20660  filuni  20676  ufileu  20710  rescncf  21691  shmodsi  26707  spanuni  26862  spansneleq  26888  mdi  27613  dmdi  27620  dmdi4  27625  funimass4f  27903  bj-ax89  30789  ffnafv  37605