Theorem sylan9r 658

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem sylan9r

Step	Hyp	Ref	Expression
1		sylan9r.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		sylan9r.2	. . 3 |- ( th -> ( ch -> ta ) )
3	1, 2	syl9r 72	. 2 |- ( th -> ( ph -> ( ps -> ta ) ) )
4	3	imp 429	1 |- ( ( th /\ ph ) -> ( 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:  spimt  1967  limsssuc  6656  tfindsg  6666  findsg  6698  f1oweALT  6758  oaordi  7185  pssnn  7728  inf3lem2  8035  cardlim  8342  ac10ct  8404  cardaleph  8459  cfub  8618  cfcoflem  8641  hsmexlem2  8796  zorn2lem7  8871  pwcfsdom  8947  grur1a  9186  genpcd  9373  supmul  10500  zeo  10935  uzwo  11133  uzwoOLD  11134  xrub  11492  iccsupr  11606  climuni  13324  efgi2  16532  opnnei  19380  tgcn  19512  uffix  20150  alexsubALTlem2  20276  alexsubALT  20279  metrest  20755  causs  21465  subgoablo  24839  ocin  25740  spanuni  25988  superpos  26799  3orel13  28419  trpredmintr  28741  frmin  28749  nndivsub  29349  supadd  29469  locfincf  29629  cover2  29658  metf1o  29702  stoweidlem62  31181  bnj518  32898  bj-spimtv  33235