Theorem ad2antrl 490

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

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

Proof of Theorem ad2antrl

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantl 277	1 |- ( ( ch /\ ( ph /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simprl  529  simprll  537  simprlr  538  elxp5  5172  f1oprg  5568  elovmporab1w  6149  cnvf1olem  6312  tfrcl  6452  nnaordi  6596  swoer  6650  0er  6656  pw2f1odclem  6933  mapxpen  6947  fict  6967  dif1enen  6979  php5fin  6981  fin0  6984  fin0or  6985  diffisn  6992  infnfi  6994  unsnfi  7018  fidcenumlemrk  7058  sbthlemi8  7068  fiuni  7082  supmoti  7097  eldju2ndl  7176  eldju2ndr  7177  omp1eomlem  7198  difinfsnlem  7203  ctmlemr  7212  nninfninc  7227  nninfwlpor  7278  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  enq0sym  7547  nqnq0pi  7553  addlocpr  7651  nqprl  7666  addnqprlemrl  7672  addnqprlemru  7673  mulnqprlemrl  7688  mulnqprlemru  7689  archpr  7758  cauappcvgprlemloc  7767  cauappcvgprlemladdfl  7770  archrecpr  7779  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprprlemml  7809  caucvgprprlemopl  7812  caucvgprprlemdisj  7817  caucvgprprlemloc  7818  suplocexprlemmu  7833  suplocexprlemdisj  7835  mulcmpblnrlemg  7855  caucvgsrlemgt1  7910  axarch  8006  axcaucvglemres  8014  cnegexlem2  8250  mulge0  8694  divdivap1  8798  divdivap2  8799  conjmulap  8804  ltdivmul  8951  nn0ge0div  9462  peano2uz2  9482  peano5uzti  9483  eluzp1m1  9674  xleadd1a  9997  iooshf  10076  divelunit  10126  eluzgtdifelfzo  10328  zsupcllemex  10375  ioom  10405  modqcyc2  10507  modaddmodup  10534  uzennn  10583  seq3fveq2  10622  seqfveq2g  10624  seq3id2  10673  seqfeq3  10676  expineg2  10695  mulexpzap  10726  leexp2r  10740  expnlbnd2  10812  hashfacen  10983  wrdred1hash  11039  ccatsymb  11061  swrdwrdsymbg  11120  swrdsb0eq  11121  ccatpfx  11155  resqrexlemp1rp  11350  resqrexlemfp1  11353  negfi  11572  climcaucn  11695  fsum3cvg3  11740  fsum2dlemstep  11778  mptfzshft  11786  expcnvre  11847  fprodrev  11963  fprod2dlemstep  11966  moddvds  12143  dvdsflip  12195  addmodlteqALT  12203  nn0o  12251  dfgcd2  12368  lcmgcdlem  12432  cncongr1  12458  prmind2  12475  isprm5lem  12496  isprm6  12502  cncongrprm  12512  oddpwdclemdc  12528  sqrt2irrap  12535  hashdvds  12576  crth  12579  prmdiveq  12591  hashgcdlem  12593  hashgcdeq  12595  pclem0  12642  pclemub  12643  pcprendvds2  12647  pcmul  12657  pcexp  12665  pcneg  12681  pc2dvds  12686  pcmpt  12699  prmpwdvds  12711  pockthg  12713  1arith  12723  4sqlem2  12745  4sqlemafi  12751  4sqlem11  12757  ennnfonelemex  12818  setscom  12905  subsubm  13348  insubm  13350  isgrpinv  13419  subsubg  13566  subsubrng  14009  subsubrg  14040  islss4  14177  znf1o  14446  znidomb  14453  tgcl  14569  lmbr2  14719  txcn  14780  txdis1cn  14783  txlm  14784  hmeoimaf1o  14819  txhmeo  14824  bl2in  14908  blssps  14932  blss  14933  blssexps  14934  blssex  14935  bdxmet  15006  xmetxp  15012  xmetxpbl  15013  xmettx  15015  metcnp3  15016  metcnpi3  15022  dedekindicc  15138  ivthdichlem  15156  limcimolemlt  15169  dvmptfsum  15230  rprelogbmul  15460  logbgcd1irr  15472  mpodvdsmulf1o  15495  lgsne0  15548  gausslemma2dlem1a  15568  lgseisenlem2  15581  lgsquadlemsfi  15585  lgsquadlem1  15587  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad2lem2  15592  2sqlem8  15633  2omap  15969  qdencn  16003  trilpolemlt1  16017