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  531  simprll  539  simprlr  540  elxp5  5251  f1oprg  5660  elovmporab1w  6255  cnvf1olem  6420  ressuppss  6454  tfrcl  6595  nnaordi  6741  swoer  6795  0er  6801  modom  7061  pw2f1odclem  7087  mapxpen  7101  mapunen  7104  fict  7123  dif1enen  7137  php5fin  7139  fin0  7142  fin0or  7143  diffisn  7150  infnfi  7152  unsnfi  7179  fidcenumlemrk  7224  sbthlemi8  7234  fiuni  7265  2omap  7269  supmoti  7284  eldju2ndl  7363  eldju2ndr  7364  omp1eomlem  7385  difinfsnlem  7390  ctmlemr  7399  nninfninc  7414  nninfwlpor  7465  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  enq0sym  7747  nqnq0pi  7753  addlocpr  7851  nqprl  7866  addnqprlemrl  7872  addnqprlemru  7873  mulnqprlemrl  7888  mulnqprlemru  7889  archpr  7958  cauappcvgprlemloc  7967  cauappcvgprlemladdfl  7970  archrecpr  7979  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprprlemml  8009  caucvgprprlemopl  8012  caucvgprprlemdisj  8017  caucvgprprlemloc  8018  suplocexprlemmu  8033  suplocexprlemdisj  8035  mulcmpblnrlemg  8055  caucvgsrlemgt1  8110  axarch  8206  axcaucvglemres  8214  cnegexlem2  8449  mulge0  8893  divdivap1  8997  divdivap2  8998  conjmulap  9003  ltdivmul  9150  nn0ge0div  9665  peano2uz2  9685  peano5uzti  9686  eluzp1m1  9878  xleadd1a  10206  iooshf  10285  divelunit  10335  eluzgtdifelfzo  10542  zsupcllemex  10590  ioom  10620  modqcyc2  10722  modaddmodup  10749  uzennn  10798  seq3fveq2  10837  seqfveq2g  10839  seq3id2  10888  seqfeq3  10891  expineg2  10910  mulexpzap  10941  leexp2r  10955  expnlbnd2  11027  hashmap  11192  sseqn  11203  hashfibclem  11206  hashfacen  11208  wrdred1hash  11268  ccatsymb  11290  swrdwrdsymbg  11356  swrdsb0eq  11357  ccatpfx  11393  swrdswrd  11397  wrdind  11414  wrd2ind  11415  swrdccatin1  11417  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  resqrexlemp1rp  11691  resqrexlemfp1  11694  negfi  11913  climcaucn  12036  fsum3cvg3  12082  fsum2dlemstep  12120  mptfzshft  12128  expcnvre  12189  fprodrev  12305  fprod2dlemstep  12308  moddvds  12485  dvdsflip  12537  addmodlteqALT  12545  nn0o  12593  dfgcd2  12710  lcmgcdlem  12774  cncongr1  12800  prmind2  12817  isprm5lem  12838  isprm6  12844  cncongrprm  12854  oddpwdclemdc  12870  sqrt2irrap  12877  hashdvds  12918  crth  12921  prmdiveq  12933  hashgcdlem  12935  hashgcdeq  12937  pclem0  12984  pclemub  12985  pcprendvds2  12989  pcmul  12999  pcexp  13007  pcneg  13023  pc2dvds  13028  pcmpt  13041  prmpwdvds  13053  pockthg  13055  1arith  13065  4sqlem2  13087  4sqlemafi  13093  4sqlem11  13099  ennnfonelemex  13165  setscom  13252  subsubm  13696  insubm  13698  isgrpinv  13767  subsubg  13914  subsubrng  14359  subsubrg  14390  islss4  14530  znf1o  14799  znidomb  14806  tgcl  14929  lmbr2  15079  txcn  15140  txdis1cn  15143  txlm  15144  hmeoimaf1o  15179  txhmeo  15184  bl2in  15268  blssps  15292  blss  15293  blssexps  15294  blssex  15295  bdxmet  15366  xmetxp  15372  xmetxpbl  15373  xmettx  15375  metcnp3  15376  metcnpi3  15382  dedekindicc  15498  ivthdichlem  15516  limcimolemlt  15529  dvmptfsum  15590  rprelogbmul  15820  logbgcd1irr  15832  mpodvdsmulf1o  15858  lgsne0  15911  gausslemma2dlem1a  15931  lgseisenlem2  15944  lgsquadlemsfi  15948  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem2  15955  2sqlem8  15996  uspgredg2vlem  16215  subuhgr  16267  subupgr  16268  subumgr  16269  iswlkg  16324  wlkl1loop  16353  upgriswlkdc  16355  clwwlkccatlem  16395  clwwlkn1loopb  16415  clwwlknonex2e  16435  qdencn  16807  trilpolemlt1  16825