Theorem sylan9r 656

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 427	1 |- ( ( th /\ ph ) -> ( 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:  spimt  2010  limsssuc  6658  tfindsg  6668  findsg  6700  f1oweALT  6757  oaordi  7187  pssnn  7731  inf3lem2  8037  cardlim  8344  ac10ct  8406  cardaleph  8461  cfub  8620  cfcoflem  8643  hsmexlem2  8798  zorn2lem7  8873  pwcfsdom  8949  grur1a  9186  genpcd  9373  supmul  10506  zeo  10944  uzwo  11145  uzwoOLD  11146  xrub  11506  iccsupr  11620  reuccats1lem  12696  climuni  13457  efgi2  16942  opnnei  19788  tgcn  19920  locfincf  20198  uffix  20588  alexsubALTlem2  20714  alexsubALT  20717  metrest  21193  causs  21903  subgoablo  25511  ocin  26412  spanuni  26660  superpos  27471  3orel13  29335  trpredmintr  29554  frmin  29562  nndivsub  30150  supadd  30282  cover2  30444  metf1o  30488  stoweidlem62  32083  reuccatpfxs1lem  32661  bnj518  34345  bj-spimtv  34679