Theorem ad2ant2lr 747

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
ad2ant2lr	|- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrr 716	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantll 713	1 |- ( ( ( th /\ ph ) /\ ( ps /\ ta ) ) -> ch )

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:  reusv2lem2  4635  mpteqb  5951  omxpenlem  7616  fineqvlem  7732  marypha1lem  7891  fin23lem26  8703  axdc3lem4  8831  mulcmpblnr  9446  ltsrpr  9452  sub4  9864  muladd  9990  ltleadd  10036  divdivdiv  10246  divadddiv  10260  ltmul12a  10399  lt2mul2div  10422  xlemul1a  11484  fzrev  11746  facndiv  12340  fsumconst  13579  isprm5  14125  acsfn2  14932  ghmeql  16158  subgdmdprd  16949  lssvsubcl  17458  lssvacl  17468  lidlsubclOLD  17731  ocvin  18572  lindfmm  18729  scmatghm  18902  scmatmhm  18903  slesolinv  19049  slesolinvbi  19050  slesolex  19051  pm2mpf1lem  19162  pm2mpcoe1  19168  reftr  19881  alexsubALTlem2  20414  alexsubALTlem3  20415  blbas  20799  nmoco  21110  cncfmet  21278  cmetcaulem  21593  mbflimsup  21939  ulmdvlem3  22662  ptolemy  22754  grpoideu  25076  ipblnfi  25636  htthlem  25699  hvaddsub4  25860  bralnfn  26732  hmops  26804  hmopm  26805  adjadd  26877  opsqrlem1  26924  atomli  27166  chirredlem2  27175  atcvat3i  27180  mdsymlem5  27191  cdj1i  27217  derangenlem  28481  elmrsubrn  28746  fprodconst  29076  dfon2lem6  29188  poseq  29301  sltsolem1  29396  mblfinlem1  30019  prdsbnd  30257  heibor1lem  30273  congneg  30875  jm2.26  30912  stoweidlem34  31701  lindslinindsimp2  32774  hl2at  34831