Theorem ad2antrl 494

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  535  simprll  543  simprlr  544  elxp5  5271  f1oprg  5680  elovmporab1w  6280  cnvf1olem  6450  ressuppss  6484  tfrcl  6625  nnaordi  6771  swoer  6825  0er  6831  modom  7098  pw2f1odclem  7124  mapxpen  7138  mapunen  7141  fict  7160  dif1enen  7174  php5fin  7176  fin0  7179  fin0or  7180  diffisn  7187  infnfi  7189  unsnfi  7216  fidcenumlemrk  7261  sbthlemi8  7271  fiuni  7302  2omap  7308  supmoti  7323  eldju2ndl  7402  eldju2ndr  7403  omp1eomlem  7424  difinfsnlem  7429  ctmlemr  7438  nninfninc  7453  nninfwlpor  7504  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  enq0sym  7789  nqnq0pi  7795  addlocpr  7893  nqprl  7908  addnqprlemrl  7914  addnqprlemru  7915  mulnqprlemrl  7930  mulnqprlemru  7931  archpr  8000  cauappcvgprlemloc  8009  cauappcvgprlemladdfl  8012  archrecpr  8021  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprprlemml  8051  caucvgprprlemopl  8054  caucvgprprlemdisj  8059  caucvgprprlemloc  8060  suplocexprlemmu  8075  suplocexprlemdisj  8077  mulcmpblnrlemg  8097  caucvgsrlemgt1  8152  axarch  8248  axcaucvglemres  8256  cnegexlem2  8492  mulge0  8937  divdivap1  9043  divdivap2  9044  conjmulap  9049  ltdivmul  9196  nn0ge0div  9712  peano2uz2  9732  peano5uzti  9733  eluzp1m1  9925  xleadd1a  10254  iooshf  10333  divelunit  10383  eluzgtdifelfzo  10593  zsupcllemex  10641  infssfzcldc  10647  infssfzledc  10648  ioom  10673  modqcyc2  10775  modaddmodup  10802  uzennn  10851  seq3fveq2  10890  seqfveq2g  10892  seq3id2  10941  seqfeq3  10944  expineg2  10963  mulexpzap  10994  leexp2r  11008  expnlbnd2  11081  hashmap  11246  sseqn  11257  hashfibclem  11260  hashfacen  11262  hashf1lem2  11264  hashf1  11265  wrdred1hash  11326  ccatsymb  11348  swrdwrdsymbg  11414  swrdsb0eq  11415  ccatpfx  11451  swrdswrd  11455  wrdind  11472  wrd2ind  11473  swrdccatin1  11475  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  resqrexlemp1rp  11750  resqrexlemfp1  11753  negfi  11972  climcaucn  12095  fsum3cvg3  12141  fsum2dlemstep  12179  mptfzshft  12187  expcnvre  12248  fprodrev  12364  fprod2dlemstep  12367  moddvds  12544  dvdsflip  12596  addmodlteqALT  12604  nn0o  12652  dfgcd2  12769  lcmgcdlem  12833  cncongr1  12859  prmind2  12876  isprm5lem  12897  isprm6  12903  cncongrprm  12913  oddpwdclemdc  12929  sqrt2irrap  12936  hashdvds  12977  crth  12980  prmdiveq  12992  hashgcdlem  12994  hashgcdeq  12996  pclem0  13043  pclemub  13044  pcprendvds2  13048  pcmul  13058  pcexp  13066  pcneg  13082  pc2dvds  13087  pcmpt  13100  prmpwdvds  13112  pockthg  13114  1arith  13124  4sqlem2  13146  4sqlemafi  13152  4sqlem11  13158  ballotfilemsf1o  13235  ennnfonelemex  13283  setscom  13370  subsubm  13767  insubm  13769  isgrpinv  13836  subsubg  13977  subsubrng  14495  subsubrg  14526  islss4  14691  znf1o  14958  znidomb  14965  tgcl  15088  lmbr2  15238  txcn  15299  txdis1cn  15302  txlm  15303  hmeoimaf1o  15338  txhmeo  15343  bl2in  15427  blssps  15451  blss  15452  blssexps  15453  blssex  15454  bdxmet  15525  xmetxp  15531  xmetxpbl  15532  xmettx  15534  metcnp3  15535  metcnpi3  15541  dedekindicc  15657  ivthdichlem  15675  limcimolemlt  15688  dvmptfsum  15749  rprelogbmul  15980  logbgcd1irr  15992  mpodvdsmulf1o  16018  lgsne0  16071  gausslemma2dlem1a  16091  lgseisenlem2  16104  lgsquadlemsfi  16108  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem2  16115  2sqlem8  16156  uspgredg2vlem  16375  subuhgr  16427  subupgr  16428  subumgr  16429  iswlkg  16484  wlkl1loop  16513  upgriswlkdc  16515  clwwlkccatlem  16555  clwwlkn1loopb  16575  clwwlknonex2e  16595  qdencn  16977  trilpolemlt1  16995