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  1958  limsssuc  6561  tfindsg  6571  findsg  6603  f1oweALT  6661  oaordi  7085  pssnn  7632  inf3lem2  7936  cardlim  8243  ac10ct  8305  cardaleph  8360  cfub  8519  cfcoflem  8542  hsmexlem2  8697  zorn2lem7  8772  pwcfsdom  8848  grur1a  9087  genpcd  9276  supmul  10399  zeo  10828  uzwo  11018  uzwoOLD  11019  xrub  11375  iccsupr  11483  climuni  13132  efgi2  16326  opnnei  18840  tgcn  18972  uffix  19610  alexsubALTlem2  19736  alexsubALT  19739  metrest  20215  causs  20925  subgoablo  23933  ocin  24834  spanuni  25082  superpos  25893  3orel13  27507  trpredmintr  27829  frmin  27837  nndivsub  28437  supadd  28556  locfincf  28716  cover2  28745  metf1o  28789  stoweidlem62  29995  bnj518  32179  bj-spimtv  32514