Theorem sylan9 663

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

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  rspc2  3158  rspc3v  3162  trintss  4513  copsexg  4687  chfnrn  5993  fvcofneq  6030  ffnfv  6049  f1elima  6164  onint  6622  peano5  6716  f1oweALT  6777  smoel2  7082  pssnn  7790  fiint  7848  dffi2  7937  alephnbtwn  8502  cfcof  8704  zorn2lem7  8932  suplem1pr  9477  addsrpr  9499  mulsrpr  9500  cau3lem  13417  divalglem8  14380  efgi  17369  elfrlmbasn0  19325  locfincmp  20541  tx1stc  20665  fbunfip  20884  filuni  20900  ufileu  20934  rescncf  21929  shmodsi  27042  spanuni  27197  spansneleq  27223  mdi  27948  dmdi  27955  dmdi4  27960  funimass4f  28234  bj-ax89  31276  poimirlem32  31972  ffnafv  38673