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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simprl  535  simprll  543  simprlr  544  elxp5  5276  f1oprg  5685  elovmporab1w  6290  cnvf1olem  6460  ressuppss  6494  tfrcl  6635  nnaordi  6781  swoer  6835  0er  6841  modom  7108  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  fict  7170  dif1enen  7184  php5fin  7186  fin0  7189  fin0or  7190  diffisn  7197  infnfi  7199  unsnfi  7226  fidcenumlemrk  7271  sbthlemi8  7281  fiuni  7312  2omap  7318  supmoti  7333  eldju2ndl  7412  eldju2ndr  7413  omp1eomlem  7434  difinfsnlem  7439  ctmlemr  7448  nninfninc  7463  nninfwlpor  7514  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  enq0sym  7799  nqnq0pi  7805  addlocpr  7903  nqprl  7918  addnqprlemrl  7924  addnqprlemru  7925  mulnqprlemrl  7940  mulnqprlemru  7941  archpr  8010  cauappcvgprlemloc  8019  cauappcvgprlemladdfl  8022  archrecpr  8031  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemdisj  8069  caucvgprprlemloc  8070  suplocexprlemmu  8085  suplocexprlemdisj  8087  mulcmpblnrlemg  8107  caucvgsrlemgt1  8162  axarch  8258  axcaucvglemres  8266  cnegexlem2  8503  mulge0  8949  divdivap1  9055  divdivap2  9056  conjmulap  9061  ltdivmul  9208  nn0ge0div  9737  peano2uz2  9757  peano5uzti  9758  eluzp1m1  9955  xleadd1a  10285  iooshf  10364  divelunit  10414  eluzgtdifelfzo  10625  zsupcllemex  10673  infssfzcldc  10679  infssfzledc  10680  ioom  10705  modqcyc2  10810  modaddmodup  10837  uzennn  10886  seq3fveq2  10925  seqfveq2g  10927  seq3id2  10976  seqfeq3  10979  expineg2  10998  mulexpzap  11029  leexp2r  11043  expnlbnd2  11116  hashmap  11282  sseqn  11293  hashfibclem  11296  hashfacen  11298  hashf1lem2  11300  hashf1  11301  wrdred1hash  11362  ccatsymb  11384  swrdwrdsymbg  11450  swrdsb0eq  11451  ccatpfx  11487  swrdswrd  11491  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  resqrexlemp1rp  11786  resqrexlemfp1  11789  negfi  12009  climcaucn  12133  fsum3cvg3  12179  fsum2dlemstep  12217  mptfzshft  12225  expcnvre  12286  fprodrev  12402  fprod2dlemstep  12405  moddvds  12582  dvdsflip  12634  addmodlteqALT  12642  nn0o  12690  dfgcd2  12807  lcmgcdlem  12871  cncongr1  12897  prmind2  12914  isprm5lem  12936  isprm6  12942  cncongrprm  12952  pwbdvdslemn  12960  nnmaxpw  12969  sqrt2irrap  12976  nn0sqdcq  13004  sqrtrirr  13005  hashdvds  13019  crth  13022  prmdiveq  13034  hashgcdlem  13036  hashgcdeq  13038  pclem0  13085  pclemub  13086  pcprendvds2  13090  pcmul  13100  pcexp  13108  pcneg  13124  pc2dvds  13129  pcmpt  13142  prmpwdvds  13154  pockthg  13156  1arith  13166  4sqlem2  13188  4sqlemafi  13194  4sqlem11  13200  ballotfilemsf1o  13306  ennnfonelemex  13354  setscom  13441  subsubm  13839  insubm  13841  isgrpinv  13908  subsubg  14049  subsubrng  14571  subsubrg  14602  islss4  14768  znf1o  15035  znidomb  15042  issubassa3  15061  tgcl  15214  lmbr2  15364  txcn  15425  txdis1cn  15428  txlm  15429  hmeoimaf1o  15464  txhmeo  15469  bl2in  15553  blssps  15577  blss  15578  blssexps  15579  blssex  15580  bdxmet  15651  xmetxp  15657  xmetxpbl  15658  xmettx  15660  metcnp3  15661  metcnpi3  15667  dedekindicc  15783  ivthdichlem  15801  limcimolemlt  15814  dvmptfsum  15875  rprelogbmul  16110  logbgcd1irr  16122  mpodvdsmulf1o  16185  lgsne0  16255  gausslemma2dlem1a  16275  lgseisenlem2  16288  lgsquadlemsfi  16292  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem2  16299  2sqlem8  16340  uspgredg2vlem  16559  subuhgr  16611  subupgr  16612  subumgr  16613  iswlkg  16668  wlkl1loop  16697  upgriswlkdc  16699  clwwlkccatlem  16739  clwwlkn1loopb  16759  clwwlknonex2e  16779  qdencn  17170  trilpolemlt1  17188