Theorem sylan9r 664

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 431	1 |- ( ( th /\ ph ) -> ( ps -> ta ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  spimt  2097  limsssuc  6677  tfindsg  6687  findsg  6720  f1oweALT  6777  oaordi  7247  pssnn  7790  inf3lem2  8134  cardlim  8406  ac10ct  8465  cardaleph  8520  cfub  8679  cfcoflem  8702  hsmexlem2  8857  zorn2lem7  8932  pwcfsdom  9008  grur1a  9244  genpcd  9431  supadd  10575  supmul  10579  zeo  11021  uzwo  11222  xrub  11597  iccsupr  11727  reuccats1lem  12836  climuni  13616  efgi2  17375  opnnei  20136  tgcn  20268  locfincf  20546  uffix  20936  alexsubALTlem2  21063  alexsubALT  21066  metrest  21539  causs  22268  subgoablo  26039  ocin  26949  spanuni  27197  superpos  28007  bnj518  29697  3orel13  30349  trpredmintr  30472  frmin  30480  nndivsub  31117  bj-spimtv  31319  cover2  32040  metf1o  32084  intabssd  36216  stoweidlem62  37923  stoweidlem62OLD  37924  reuccatpfxs1lem  38974