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  5256  f1oprg  5665  elovmporab1w  6263  cnvf1olem  6433  ressuppss  6467  tfrcl  6608  nnaordi  6754  swoer  6808  0er  6814  modom  7074  pw2f1odclem  7100  mapxpen  7114  mapunen  7117  fict  7136  dif1enen  7150  php5fin  7152  fin0  7155  fin0or  7156  diffisn  7163  infnfi  7165  unsnfi  7192  fidcenumlemrk  7237  sbthlemi8  7247  fiuni  7278  2omap  7282  supmoti  7297  eldju2ndl  7376  eldju2ndr  7377  omp1eomlem  7398  difinfsnlem  7403  ctmlemr  7412  nninfninc  7427  nninfwlpor  7478  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  enq0sym  7763  nqnq0pi  7769  addlocpr  7867  nqprl  7882  addnqprlemrl  7888  addnqprlemru  7889  mulnqprlemrl  7904  mulnqprlemru  7905  archpr  7974  cauappcvgprlemloc  7983  cauappcvgprlemladdfl  7986  archrecpr  7995  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemdisj  8033  caucvgprprlemloc  8034  suplocexprlemmu  8049  suplocexprlemdisj  8051  mulcmpblnrlemg  8071  caucvgsrlemgt1  8126  axarch  8222  axcaucvglemres  8230  cnegexlem2  8465  mulge0  8910  divdivap1  9014  divdivap2  9015  conjmulap  9020  ltdivmul  9167  nn0ge0div  9683  peano2uz2  9703  peano5uzti  9704  eluzp1m1  9896  xleadd1a  10225  iooshf  10304  divelunit  10354  eluzgtdifelfzo  10564  zsupcllemex  10612  infssfzcldc  10618  infssfzledc  10619  ioom  10644  modqcyc2  10746  modaddmodup  10773  uzennn  10822  seq3fveq2  10861  seqfveq2g  10863  seq3id2  10912  seqfeq3  10915  expineg2  10934  mulexpzap  10965  leexp2r  10979  expnlbnd2  11052  hashmap  11217  sseqn  11228  hashfibclem  11231  hashfacen  11233  wrdred1hash  11293  ccatsymb  11315  swrdwrdsymbg  11381  swrdsb0eq  11382  ccatpfx  11418  swrdswrd  11422  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  resqrexlemp1rp  11716  resqrexlemfp1  11719  negfi  11938  climcaucn  12061  fsum3cvg3  12107  fsum2dlemstep  12145  mptfzshft  12153  expcnvre  12214  fprodrev  12330  fprod2dlemstep  12333  moddvds  12510  dvdsflip  12562  addmodlteqALT  12570  nn0o  12618  dfgcd2  12735  lcmgcdlem  12799  cncongr1  12825  prmind2  12842  isprm5lem  12863  isprm6  12869  cncongrprm  12879  oddpwdclemdc  12895  sqrt2irrap  12902  hashdvds  12943  crth  12946  prmdiveq  12958  hashgcdlem  12960  hashgcdeq  12962  pclem0  13009  pclemub  13010  pcprendvds2  13014  pcmul  13024  pcexp  13032  pcneg  13048  pc2dvds  13053  pcmpt  13066  prmpwdvds  13078  pockthg  13080  1arith  13090  4sqlem2  13112  4sqlemafi  13118  4sqlem11  13124  ballotfilemsf1o  13201  ennnfonelemex  13249  setscom  13336  subsubm  13738  insubm  13740  isgrpinv  13809  subsubg  13950  subsubrng  14460  subsubrg  14491  islss4  14656  znf1o  14925  znidomb  14932  tgcl  15055  lmbr2  15205  txcn  15266  txdis1cn  15269  txlm  15270  hmeoimaf1o  15305  txhmeo  15310  bl2in  15394  blssps  15418  blss  15419  blssexps  15420  blssex  15421  bdxmet  15492  xmetxp  15498  xmetxpbl  15499  xmettx  15501  metcnp3  15502  metcnpi3  15508  dedekindicc  15624  ivthdichlem  15642  limcimolemlt  15655  dvmptfsum  15716  rprelogbmul  15946  logbgcd1irr  15958  mpodvdsmulf1o  15984  lgsne0  16037  gausslemma2dlem1a  16057  lgseisenlem2  16070  lgsquadlemsfi  16074  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad2lem2  16081  2sqlem8  16122  uspgredg2vlem  16341  subuhgr  16393  subupgr  16394  subumgr  16395  iswlkg  16450  wlkl1loop  16479  upgriswlkdc  16481  clwwlkccatlem  16521  clwwlkn1loopb  16541  clwwlknonex2e  16561  qdencn  16933  trilpolemlt1  16951