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  1989  limsssuc  6666  tfindsg  6676  findsg  6708  f1oweALT  6765  oaordi  7193  pssnn  7736  inf3lem2  8044  cardlim  8351  ac10ct  8413  cardaleph  8468  cfub  8627  cfcoflem  8650  hsmexlem2  8805  zorn2lem7  8880  pwcfsdom  8956  grur1a  9195  genpcd  9382  supmul  10512  zeo  10949  uzwo  11148  uzwoOLD  11149  xrub  11507  iccsupr  11621  reuccats1lem  12679  climuni  13349  efgi2  16612  opnnei  19487  tgcn  19619  locfincf  19898  uffix  20288  alexsubALTlem2  20414  alexsubALT  20417  metrest  20893  causs  21603  subgoablo  25178  ocin  26079  spanuni  26327  superpos  27138  3orel13  28960  trpredmintr  29282  frmin  29290  nndivsub  29890  supadd  30010  cover2  30172  metf1o  30216  stoweidlem62  31729  bnj518  33651  bj-spimtv  33992