Theorem sylan9r 690

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  spimt  2253  limsssuc  7050  tfindsg  7060  findsg  7093  f1oweALT  7152  oaordi  7626  pssnn  8178  inf3lem2  8526  cardlim  8798  ac10ct  8857  cardaleph  8912  cfub  9071  cfcoflem  9094  hsmexlem2  9249  zorn2lem7  9324  pwcfsdom  9405  grur1a  9641  genpcd  9828  supadd  10991  supmul  10995  zeo  11463  uzwo  11751  xrub  12142  iccsupr  12266  reuccats1lem  13479  climuni  14283  efgi2  18138  opnnei  20924  tgcn  21056  locfincf  21334  uffix  21725  alexsubALTlem2  21852  alexsubALT  21855  metrest  22329  causs  23096  ocin  28155  spanuni  28403  superpos  29213  bnj518  30956  3orel13  31598  trpredmintr  31731  frmin  31739  nndivsub  32456  bj-spimtv  32718  bj-snmoore  33068  cover2  33508  metf1o  33551  intabssd  37916  stoweidlem62  40279  reuccatpfxs1lem  41433