Theorem sylan9r 662

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  spimt  2058  limsssuc  6682  tfindsg  6692  findsg  6725  f1oweALT  6782  oaordi  7246  pssnn  7787  inf3lem2  8125  cardlim  8396  ac10ct  8454  cardaleph  8509  cfub  8668  cfcoflem  8691  hsmexlem2  8846  zorn2lem7  8921  pwcfsdom  8997  grur1a  9233  genpcd  9420  supadd  10564  supmul  10568  zeo  11010  uzwo  11211  xrub  11586  iccsupr  11716  reuccats1lem  12810  climuni  13583  efgi2  17303  opnnei  20060  tgcn  20192  locfincf  20470  uffix  20860  alexsubALTlem2  20987  alexsubALT  20990  metrest  21463  causs  22154  subgoablo  25881  ocin  26781  spanuni  27029  superpos  27839  bnj518  29482  3orel13  30134  trpredmintr  30256  frmin  30264  nndivsub  30899  bj-spimtv  31055  cover2  31744  metf1o  31788  stoweidlem62  37496  stoweidlem62OLD  37497  reuccatpfxs1lem  38377