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  5217  f1oprg  5617  elovmporab1w  6206  cnvf1olem  6370  tfrcl  6510  nnaordi  6654  swoer  6708  0er  6714  pw2f1odclem  6995  mapxpen  7009  fict  7030  dif1enen  7042  php5fin  7044  fin0  7047  fin0or  7048  diffisn  7055  infnfi  7057  unsnfi  7081  fidcenumlemrk  7121  sbthlemi8  7131  fiuni  7145  supmoti  7160  eldju2ndl  7239  eldju2ndr  7240  omp1eomlem  7261  difinfsnlem  7266  ctmlemr  7275  nninfninc  7290  nninfwlpor  7341  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  enq0sym  7619  nqnq0pi  7625  addlocpr  7723  nqprl  7738  addnqprlemrl  7744  addnqprlemru  7745  mulnqprlemrl  7760  mulnqprlemru  7761  archpr  7830  cauappcvgprlemloc  7839  cauappcvgprlemladdfl  7842  archrecpr  7851  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprprlemml  7881  caucvgprprlemopl  7884  caucvgprprlemdisj  7889  caucvgprprlemloc  7890  suplocexprlemmu  7905  suplocexprlemdisj  7907  mulcmpblnrlemg  7927  caucvgsrlemgt1  7982  axarch  8078  axcaucvglemres  8086  cnegexlem2  8322  mulge0  8766  divdivap1  8870  divdivap2  8871  conjmulap  8876  ltdivmul  9023  nn0ge0div  9534  peano2uz2  9554  peano5uzti  9555  eluzp1m1  9746  xleadd1a  10069  iooshf  10148  divelunit  10198  eluzgtdifelfzo  10403  zsupcllemex  10450  ioom  10480  modqcyc2  10582  modaddmodup  10609  uzennn  10658  seq3fveq2  10697  seqfveq2g  10699  seq3id2  10748  seqfeq3  10751  expineg2  10770  mulexpzap  10801  leexp2r  10815  expnlbnd2  10887  hashfacen  11058  wrdred1hash  11115  ccatsymb  11137  swrdwrdsymbg  11196  swrdsb0eq  11197  ccatpfx  11233  swrdswrd  11237  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  resqrexlemp1rp  11517  resqrexlemfp1  11520  negfi  11739  climcaucn  11862  fsum3cvg3  11907  fsum2dlemstep  11945  mptfzshft  11953  expcnvre  12014  fprodrev  12130  fprod2dlemstep  12133  moddvds  12310  dvdsflip  12362  addmodlteqALT  12370  nn0o  12418  dfgcd2  12535  lcmgcdlem  12599  cncongr1  12625  prmind2  12642  isprm5lem  12663  isprm6  12669  cncongrprm  12679  oddpwdclemdc  12695  sqrt2irrap  12702  hashdvds  12743  crth  12746  prmdiveq  12758  hashgcdlem  12760  hashgcdeq  12762  pclem0  12809  pclemub  12810  pcprendvds2  12814  pcmul  12824  pcexp  12832  pcneg  12848  pc2dvds  12853  pcmpt  12866  prmpwdvds  12878  pockthg  12880  1arith  12890  4sqlem2  12912  4sqlemafi  12918  4sqlem11  12924  ennnfonelemex  12985  setscom  13072  subsubm  13516  insubm  13518  isgrpinv  13587  subsubg  13734  subsubrng  14178  subsubrg  14209  islss4  14346  znf1o  14615  znidomb  14622  tgcl  14738  lmbr2  14888  txcn  14949  txdis1cn  14952  txlm  14953  hmeoimaf1o  14988  txhmeo  14993  bl2in  15077  blssps  15101  blss  15102  blssexps  15103  blssex  15104  bdxmet  15175  xmetxp  15181  xmetxpbl  15182  xmettx  15184  metcnp3  15185  metcnpi3  15191  dedekindicc  15307  ivthdichlem  15325  limcimolemlt  15338  dvmptfsum  15399  rprelogbmul  15629  logbgcd1irr  15641  mpodvdsmulf1o  15664  lgsne0  15717  gausslemma2dlem1a  15737  lgseisenlem2  15750  lgsquadlemsfi  15754  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad2lem2  15761  2sqlem8  15802  uspgredg2vlem  16018  iswlkg  16041  wlkl1loop  16069  upgriswlkdc  16071  2omap  16359  qdencn  16395  trilpolemlt1  16409