Theorem ad2antrr 488

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad2antrr	|- ( ( ( ph /\ ch ) /\ th ) -> ps )

Proof of Theorem ad2antrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantlr 477	1 |- ( ( ( ph /\ ch ) /\ 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:  ad3antrrr  492  ad5ant13  519  ad5ant23  522  simpll  527  simplll  533  simpllr  534  ad5ant123  1241  vtoclgft  2814  reupick  3447  euotd  4287  frirrg  4385  ralxfrd  4497  nnsucpred  4653  foun  5523  f1oprg  5548  dffo4  5710  foeqcnvco  5837  fliftfun  5843  isotr  5863  riotass2  5904  ovmpodxf  6048  mpoxopoveq  6298  tfrlem1  6366  tfrlemibacc  6384  tfrlemibfn  6386  tfrlemi14d  6391  tfrexlem  6392  tfr1onlembacc  6400  tfr1onlembfn  6402  tfr1onlemres  6407  tfrcllembacc  6413  tfrcllembfn  6415  tfrcllemres  6420  frecabcl  6457  nnmordi  6574  eroprf  6687  f1imaen2g  6852  pw2f1odclem  6895  xpen  6906  mapen  6907  mapdom1g  6908  mapxpen  6909  xpmapenlem  6910  phplem4dom  6923  nndomo  6925  phpm  6926  fidifsnen  6931  dif1enen  6941  fisbth  6944  fimax2gtrilemstep  6961  fimax2gtri  6962  en2eqpr  6968  unsnfidcex  6981  unsnfidcel  6982  ssfirab  6997  fidcenumlemrks  7019  sbthlemi8  7030  fiuni  7044  ordiso2  7101  updjud  7148  difinfsnlem  7165  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  enumct  7181  nnnninfeq  7194  nninfisol  7199  enomnilem  7204  fodju0  7213  enmkvlem  7227  enwomnilem  7235  nninfwlpoimlemg  7241  exmidfodomrlemim  7268  exmidontriimlem2  7289  exmidapne  7327  cc3  7335  dfplpq2  7421  nqpi  7445  nqnq0pi  7505  nq0nn  7509  elinp  7541  elnp1st2nd  7543  genprndl  7588  genprndu  7589  addnqprllem  7594  addnqprulem  7595  addnqprl  7596  addnqpru  7597  addlocpr  7603  nqprloc  7612  prmuloc  7633  mulnqprl  7635  mulnqpru  7636  mullocpr  7638  distrlem1prl  7649  distrlem1pru  7650  ltsopr  7663  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  aptiprleml  7706  aptiprlemu  7707  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  archrecpr  7731  caucvgprlemnkj  7733  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnjltk  7758  caucvgprprlemml  7761  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemdisj  7769  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  caucvgprprlemaddq  7775  suplocexprlemru  7786  suplocexprlemloc  7788  suplocexprlemex  7789  suplocexprlemub  7790  suplocexprlemlub  7791  mulgt0sr  7845  caucvgsrlemcau  7860  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axcaucvglemcau  7965  axcaucvglemres  7966  axpre-suploclemres  7968  axsuploc  8099  cnegexlem1  8201  cnegex  8204  apsym  8633  apcotr  8634  apadd1  8635  mulext1  8639  mulge0  8646  apti  8649  aprcl  8673  conjmulap  8756  lemulge11  8893  creui  8987  nndiv  9031  zaddcllemneg  9365  suprzclex  9424  eluzuzle  9609  infregelbex  9672  divfnzn  9695  qapne  9713  xrltso  9871  xnn0dcle  9877  xnn0letri  9878  xrre  9895  xrre3  9897  xaddf  9919  xaddval  9920  xpncan  9946  xleadd1a  9948  xltadd1  9951  xleaddadd  9962  ixxss12  9981  elioc2  10011  elico2  10012  elicc2  10013  fzm1  10175  fzneuz  10176  eluzgtdifelfzo  10273  elfzonelfzo  10306  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  nninfdcex  10327  zsupssdc  10328  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemex  10339  exbtwnz  10340  modqid  10441  modqcyc2  10452  modqmuladd  10458  modqmuladdnn0  10460  modaddmodlo  10480  addmodlteq  10490  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgsuc  10506  frecuzrdgsuctlem  10515  nninfinf  10535  seq3clss  10563  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemmo  10597  iseqf1olemqf1o  10598  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  seq3f1olemqsumk  10604  seq3f1olemqsum  10605  seq3f1olemp  10607  seq3f1oleml  10608  seq3f1o  10609  seqf1oglem1  10611  seqf1oglem2  10612  seqf1og  10613  seq3id3  10616  seqfeq4g  10623  ser3ge0  10628  exp3val  10633  expap0  10661  qsqeqor  10742  modqexp  10758  nn0ltexp2  10801  facndiv  10831  faclbnd  10833  bcval5  10855  hashunlem  10896  hashun  10897  hashprg  10900  fiprsshashgt1  10909  hashfacen  10928  zfz1isolemiso  10931  zfz1isolem1  10932  seq3coll  10934  ovshftex  10984  2shfti  10996  seq3shft  11003  cjap  11071  caucvgrelemcau  11145  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniq  11160  resqrexlemdecn  11177  resqrexlemcalc3  11181  resqrexlemcvg  11184  resqrexlemoverl  11186  leabs  11239  absexpzap  11245  ltabs  11252  abslt  11253  absle  11254  maxleim  11370  maxabslemval  11373  fimaxre2  11392  minmax  11395  2zinfmin  11408  xrmaxiflemcl  11410  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemcom  11414  xrmaxltsup  11423  xrmaxadd  11426  xrminmax  11430  xrbdtri  11441  2clim  11466  climshftlemg  11467  climsqz  11500  climsqz2  11501  climrecvg1n  11513  climcvg1nlem  11514  serf0  11517  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  summodclem2  11547  zsumdc  11549  fsum3  11552  isumss  11556  fisumss  11557  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  fsumsplit  11572  sumsnf  11574  fsum2d  11600  fisum0diag2  11612  fsummulc2  11613  modfsummod  11623  fsumabs  11630  fsumrelem  11636  fsumiun  11642  geoisumr  11683  cvgratnnlemseq  11691  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodrbdclem  11736  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  fprodssdc  11755  fprodmul  11756  prodsnf  11757  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  fprodcl2lem  11770  fprodap0  11786  fprod2d  11788  fprodrec  11794  fprodap0f  11801  efcj  11838  efaddlem  11839  tanaddaplem  11903  sinltxirr  11926  nndivides  11962  dvdsext  12020  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  bitsfzolem  12118  dvdsbnd  12123  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlemzz  12169  bezoutlemaz  12170  bezoutlembz  12171  bezoutlemeu  12174  bezoutlemle  12175  bezoutlemsup  12176  dfgcd3  12177  dfgcd2  12181  bezoutr1  12200  nnmindc  12201  nninfctlemfo  12207  dvdslcm  12237  lcmgcdlem  12245  qredeq  12264  qredeu  12265  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  isprm2lem  12284  prmind2  12288  exprmfct  12306  prmdvdsfz  12307  isprm5lem  12309  prmexpb  12319  rpexp1i  12322  sqrt2irr  12330  sqne2sq  12345  nonsq  12375  phiprmpw  12390  eulerthlemrprm  12397  eulerthlema  12398  hashgcdeq  12408  phisum  12409  modprmn0modprm0  12425  pclemub  12456  pclemdc  12457  pcmul  12470  pcqmul  12472  pcxqcl  12481  pcdvdstr  12496  pcprmpw2  12502  difsqpwdvds  12507  pcmpt  12512  oddprmdvds  12523  prmpwdvds  12524  pockthg  12526  infpnlem1  12528  1arith  12536  4sqlem2  12558  4sqlemafi  12564  4sqlemffi  12565  4sqleminfi  12566  4sqlem11  12570  4sqlem13m  12572  4sqlem14  12573  4sqlem17  12576  4sqlem18  12577  ennnfonelemg  12620  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemfun  12634  ennnfonelemf1  12635  ennnfonelemrn  12636  ennnfonelemdm  12637  ennnfonelemnn0  12639  ennnfonelemim  12641  exmidunben  12643  ctinfomlemom  12644  ctinf  12647  ctiunctlemudc  12654  nninfdclemlt  12668  nninfdclemf1  12669  isstruct2r  12689  imasival  12949  gsumpropd2  13036  sgrppropd  13056  mndpropd  13081  issubmnd  13083  mndissubm  13107  resmhm2b  13121  mhmeql  13124  gsumfzz  13127  gsumwsubmcl  13128  gsumwmhm  13130  gsumfzcl  13131  grpinvnz  13203  mhmmnd  13246  mulgfng  13254  mulgz  13280  mulgnndir  13281  mulgnn0dir  13282  mulgneg2  13286  mulgass  13289  mhmmulg  13293  issubgrpd2  13320  issubg4m  13323  grpissubg  13324  isnsg3  13337  ghmpreima  13396  ghmnsgpreima  13399  ghmf1  13403  conjnmz  13409  conjnmzb  13410  eqgabl  13460  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  rngpropd  13511  issrg  13521  ringpropd  13594  ringinvnz1ne0  13605  dvdsrvald  13649  dvdsrd  13650  dvdsrtr  13657  unitgrp  13672  rhmopp  13732  lmodfopne  13882  lmodprop2d  13904  lssvacl  13921  lsslss  13937  lss1d  13939  lsspropdg  13987  rnglidlmcl  14036  lidlacl  14040  isridl  14060  znidomb  14214  znunit  14215  znrrg  14216  psrval  14220  tgdom  14308  neipsm  14390  tgrest  14405  cnfval  14430  cnpfval  14431  cnpval  14434  iscnp4  14454  cnpnei  14455  cnptopco  14458  cncnpi  14464  cncnp  14466  cnptopresti  14474  cnptoprest2  14476  cndis  14477  lmtopcnp  14486  txbasval  14503  neitx  14504  txcnp  14507  txcnmpt  14509  txcn  14511  imasnopn  14535  psmetres2  14569  isxmet2d  14584  xblss2ps  14640  xblss2  14641  blbas  14669  neibl  14727  metss2lem  14733  metrest  14742  xmettx  14746  metcnp3  14747  metcnp  14748  metcnp2  14749  metcnpi  14751  metcnpi2  14752  mulc1cncf  14825  cncfco  14827  mulcncflem  14843  mulcncf  14844  dedekindeulemuub  14853  dedekindeulemloc  14855  dedekindeulemlu  14857  dedekindeu  14859  suplociccreex  14860  suplociccex  14861  dedekindicclemuub  14862  dedekindicclemloc  14864  dedekindicclemlu  14866  dedekindicclemicc  14868  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  ivthinc  14879  limcimolemlt  14900  limccnp2lem  14912  limccnp2cntop  14913  limccoap  14914  dvcj  14945  dvmptfsum  14961  dveflem  14962  plyf  14973  plyaddlem1  14983  plymullem1  14984  plycolemc  14994  plyco  14995  plycj  14997  dvply1  15001  dvply2g  15002  efltlemlt  15010  sin0pilem1  15017  sin0pilem2  15018  pilem3  15019  coseq0negpitopi  15072  abssinper  15082  cos02pilt1  15087  relogeftb  15101  logbgcd1irraplemexp  15204  logbgcd1irrap  15206  dvdsppwf1o  15225  mpodvdsmulf1o  15226  mersenne  15233  perfectlem2  15236  perfect  15237  lgsval  15245  lgsfvalg  15246  lgsfcl2  15247  lgsval2lem  15251  lgsmod  15267  lgsdilem  15268  lgsdir2lem4  15272  lgsdir2  15274  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem2  15323  2lgslem1a1  15327  2lgslem1a  15329  2sqlem5  15360  2sqlem6  15361  2sqlem7  15362  2sqlem9  15365  2sqlem10  15366  bj-findis  15625  pwle2  15643  pwf1oexmid  15644  pw1nct  15647  nnsf  15649  peano4nninf  15650  nninfall  15653  nninfsellemeq  15658  nninfsellemeqinf  15660  qdencn  15671  refeq  15672  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  nconstwlpolemgt0  15708  nconstwlpolem  15709  neapmkvlem  15711