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  535  simpllr  536  ad5ant123  1266  vtoclgft  2855  reupick  3493  euotd  4353  frirrg  4453  ralxfrd  4565  nnsucpred  4721  foun  5611  f1oprg  5638  dffo4  5803  funopsn  5838  foeqcnvco  5941  fliftfun  5947  isotr  5967  riotass2  6010  ovmpodxf  6157  suppfnss  6435  suppcofn  6444  mpoxopoveq  6449  tfrlem1  6517  tfrlemibacc  6535  tfrlemibfn  6537  tfrlemi14d  6542  tfrexlem  6543  tfr1onlembacc  6551  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllembacc  6564  tfrcllembfn  6566  tfrcllemres  6571  frecabcl  6608  nnmordi  6727  eroprf  6840  f1imaen2g  7010  pw2f1odclem  7063  xpen  7074  mapen  7075  mapdom1g  7076  mapxpen  7077  xpmapenlem  7078  phplem4dom  7091  nndomo  7093  phpm  7095  fidifsnen  7100  dif1enen  7112  fisbth  7115  fimax2gtrilemstep  7133  fimax2gtri  7134  eqsndc  7138  en2eqpr  7142  unsnfidcex  7155  unsnfidcel  7156  ssfirab  7172  fidcenumlemrks  7195  sbthlemi8  7206  fiuni  7237  ordiso2  7294  updjud  7341  difinfsnlem  7358  ctssdclemn0  7369  ctssdccl  7370  ctssdc  7372  enumctlemm  7373  enumct  7374  nnnninfeq  7387  nninfisol  7392  enomnilem  7397  fodju0  7406  enmkvlem  7420  enwomnilem  7428  nninfwlpoimlemg  7434  pr1or2  7459  pr2cv1  7460  exmidfodomrlemim  7472  exmidontriimlem2  7497  exmidapne  7539  cc3  7547  dfplpq2  7634  nqpi  7658  nqnq0pi  7718  nq0nn  7722  elinp  7754  elnp1st2nd  7756  genprndl  7801  genprndu  7802  addnqprllem  7807  addnqprulem  7808  addnqprl  7809  addnqpru  7810  addlocpr  7816  nqprloc  7825  prmuloc  7846  mulnqprl  7848  mulnqpru  7849  mullocpr  7851  distrlem1prl  7862  distrlem1pru  7863  ltsopr  7876  ltexprlemopl  7881  ltexprlemopu  7883  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  addcanprleml  7894  addcanprlemu  7895  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  aptiprleml  7919  aptiprlemu  7920  archpr  7923  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  archrecpr  7944  caucvgprlemnkj  7946  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemdisj  7954  caucvgprlemloc  7955  caucvgprlemladdfu  7957  caucvgprprlemnkltj  7969  caucvgprprlemnkeqj  7970  caucvgprprlemnjltk  7971  caucvgprprlemml  7974  caucvgprprlemopl  7977  caucvgprprlemlol  7978  caucvgprprlemdisj  7982  caucvgprprlemexbt  7986  caucvgprprlemexb  7987  caucvgprprlemaddq  7988  suplocexprlemru  7999  suplocexprlemloc  8001  suplocexprlemex  8002  suplocexprlemub  8003  suplocexprlemlub  8004  mulgt0sr  8058  caucvgsrlemcau  8073  caucvgsrlemoffcau  8078  caucvgsrlemoffres  8080  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axcaucvglemcau  8178  axcaucvglemres  8179  axpre-suploclemres  8181  axsuploc  8311  cnegexlem1  8413  cnegex  8416  apsym  8845  apcotr  8846  apadd1  8847  mulext1  8851  mulge0  8858  apti  8861  aprcl  8885  conjmulap  8968  lemulge11  9105  creui  9199  nndiv  9243  zaddcllemneg  9579  suprzclex  9639  eluzuzle  9825  infregelbex  9893  divfnzn  9916  qapne  9934  xrltso  10092  xnn0dcle  10098  xnn0letri  10099  xrre  10116  xrre3  10118  xaddf  10140  xaddval  10141  xpncan  10167  xleadd1a  10169  xltadd1  10172  xleaddadd  10183  ixxss12  10202  elioc2  10232  elico2  10233  elicc2  10234  fzm1  10397  fzneuz  10398  eluzgtdifelfzo  10505  elfzonelfzo  10538  exfzdc  10549  zsupcllemstep  10552  infssuzex  10556  suprzubdc  10559  nninfdcex  10560  zsupssdc  10561  qtri3or  10563  exbtwnzlemstep  10570  exbtwnzlemex  10572  exbtwnz  10573  modqid  10674  modqcyc2  10685  modqmuladd  10691  modqmuladdnn0  10693  modaddmodlo  10713  addmodlteq  10723  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgsuc  10739  frecuzrdgsuctlem  10748  nninfinf  10768  seq3clss  10796  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemmo  10830  iseqf1olemqf1o  10831  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seq3f1olemp  10840  seq3f1oleml  10841  seq3f1o  10842  seqf1oglem1  10844  seqf1oglem2  10845  seqf1og  10846  seq3id3  10849  seqfeq4g  10856  ser3ge0  10861  exp3val  10866  expap0  10894  qsqeqor  10975  modqexp  10991  nn0ltexp2  11034  facndiv  11064  faclbnd  11066  bcval5  11088  hashunlem  11130  hashun  11131  hashprg  11135  fiprsshashgt1  11144  hashfacen  11163  zfz1isolemiso  11166  zfz1isolem1  11167  seq3coll  11169  hashtpglem  11173  ccatcl  11236  ccatlen  11238  ccatvalfn  11244  ccatsymb  11245  ccatrn  11252  ccat2s1fstg  11291  swrdclg  11297  swrdspsleq  11314  pfxeq  11343  swrdswrd  11352  wrdind  11369  wrd2ind  11370  swrdccatin1  11372  swrdccatin2  11376  pfxccatin12  11380  pfxccat3  11381  swrdccat3b  11387  reuccatpfxs1  11394  ovshftex  11459  2shfti  11471  seq3shft  11478  cjap  11546  caucvgrelemcau  11620  cvg1nlemcau  11624  cvg1nlemres  11625  recvguniq  11635  resqrexlemdecn  11652  resqrexlemcalc3  11656  resqrexlemcvg  11659  resqrexlemoverl  11661  leabs  11714  absexpzap  11720  ltabs  11727  abslt  11728  absle  11729  maxleim  11845  maxabslemval  11848  fimaxre2  11867  minmax  11870  2zinfmin  11883  xrmaxiflemcl  11885  xrmaxifle  11886  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxiflemcom  11889  xrmaxltsup  11898  xrmaxadd  11901  xrminmax  11905  xrbdtri  11916  2clim  11941  climshftlemg  11942  climsqz  11975  climsqz2  11976  climrecvg1n  11988  climcvg1nlem  11989  serf0  11992  sumrbdclem  12018  fsum3cvg  12019  summodclem3  12021  summodclem2a  12022  summodclem2  12023  zsumdc  12025  fsum3  12028  isumss  12032  fisumss  12033  fsum3cvg3  12037  fsumcl2lem  12039  fsumadd  12047  fsumsplit  12048  sumsnf  12050  fsum2d  12076  fisum0diag2  12088  fsummulc2  12089  modfsummod  12099  fsumabs  12106  fsumrelem  12112  fsumiun  12118  geoisumr  12159  cvgratnnlemseq  12167  cvgratz  12173  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodrbdclem  12212  fproddccvg  12213  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodntrivap  12225  fprodssdc  12231  fprodmul  12232  prodsnf  12233  fprodsplitdc  12237  fprodsplit  12238  fprodunsn  12245  fprodcl2lem  12246  fprodap0  12262  fprod2d  12264  fprodrec  12270  fprodap0f  12277  efcj  12314  efaddlem  12315  tanaddaplem  12379  sinltxirr  12402  nndivides  12438  dvdsext  12496  divalglemeunn  12562  divalglemex  12563  divalglemeuneg  12564  bitsfzolem  12595  bitsmod  12597  bitsinv1  12603  dvdsbnd  12607  bezoutlemnewy  12647  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemzz  12653  bezoutlemaz  12654  bezoutlembz  12655  bezoutlemeu  12658  bezoutlemle  12659  bezoutlemsup  12660  dfgcd3  12661  dfgcd2  12665  bezoutr1  12684  nnmindc  12685  nninfctlemfo  12691  dvdslcm  12721  lcmgcdlem  12729  qredeq  12748  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  isprm2lem  12768  prmind2  12772  exprmfct  12790  prmdvdsfz  12791  isprm5lem  12793  prmexpb  12803  rpexp1i  12806  sqrt2irr  12814  sqne2sq  12829  nonsq  12859  phiprmpw  12874  eulerthlemrprm  12881  eulerthlema  12882  hashgcdeq  12892  phisum  12893  modprmn0modprm0  12909  pclemub  12940  pclemdc  12941  pcmul  12954  pcqmul  12956  pcxqcl  12965  pcdvdstr  12980  pcprmpw2  12986  difsqpwdvds  12991  pcmpt  12996  oddprmdvds  13007  prmpwdvds  13008  pockthg  13010  infpnlem1  13012  1arith  13020  4sqlem2  13042  4sqlemafi  13048  4sqlemffi  13049  4sqleminfi  13050  4sqlem11  13054  4sqlem13m  13056  4sqlem14  13057  4sqlem17  13060  4sqlem18  13061  ennnfonelemg  13104  ennnfoneleminc  13112  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemfun  13118  ennnfonelemf1  13119  ennnfonelemrn  13120  ennnfonelemdm  13121  ennnfonelemnn0  13123  ennnfonelemim  13125  exmidunben  13127  ctinfomlemom  13128  ctinf  13131  ctiunctlemudc  13138  nninfdclemlt  13152  nninfdclemf1  13153  isstruct2r  13173  prdsval  13436  imasival  13469  gsumpropd2  13556  sgrppropd  13576  prdssgrpd  13578  mndpropd  13603  issubmnd  13605  prdsidlem  13610  prdsmndd  13611  pws0g  13614  mndissubm  13638  resmhm2b  13652  mhmeql  13655  gsumfzz  13658  gsumwsubmcl  13659  gsumwmhm  13661  gsumfzcl  13662  grpinvnz  13734  pwssub  13776  mhmmnd  13783  mulgfng  13791  mulgz  13817  mulgnndir  13818  mulgnn0dir  13819  mulgneg2  13823  mulgass  13826  mhmmulg  13830  issubgrpd2  13857  issubg4m  13860  grpissubg  13861  isnsg3  13874  ghmpreima  13933  ghmnsgpreima  13936  ghmf1  13940  conjnmz  13946  conjnmzb  13947  eqgabl  13997  gsumfzreidx  14004  gsumfzsubmcl  14005  gsumfzmptfidmadd  14006  gsumfzmhm  14010  rngpropd  14049  issrg  14059  ringpropd  14132  ringinvnz1ne0  14143  dvdsrvald  14188  dvdsrd  14189  dvdsrtr  14196  unitgrp  14211  rhmopp  14271  lmodfopne  14422  lmodprop2d  14444  lssvacl  14461  lsslss  14477  lss1d  14479  lsspropdg  14527  rnglidlmcl  14576  lidlacl  14580  isridl  14600  znidomb  14754  znunit  14755  znrrg  14756  psrval  14762  mplsubgfilemcl  14800  mplsubgfileminv  14801  mplsubgfi  14802  tgdom  14883  neipsm  14965  tgrest  14980  cnfval  15005  cnpfval  15006  cnpval  15009  iscnp4  15029  cnpnei  15030  cnptopco  15033  cncnpi  15039  cncnp  15041  cnptopresti  15049  cnptoprest2  15051  cndis  15052  lmtopcnp  15061  txbasval  15078  neitx  15079  txcnp  15082  txcnmpt  15084  txcn  15086  imasnopn  15110  psmetres2  15144  isxmet2d  15159  xblss2ps  15215  xblss2  15216  blbas  15244  neibl  15302  metss2lem  15308  metrest  15317  xmettx  15321  metcnp3  15322  metcnp  15323  metcnp2  15324  metcnpi  15326  metcnpi2  15327  mulc1cncf  15400  cncfco  15402  mulcncflem  15418  mulcncf  15419  dedekindeulemuub  15428  dedekindeulemloc  15430  dedekindeulemlu  15432  dedekindeu  15434  suplociccreex  15435  suplociccex  15436  dedekindicclemuub  15437  dedekindicclemloc  15439  dedekindicclemlu  15441  dedekindicclemicc  15443  dedekindicc  15444  ivthinclemlopn  15447  ivthinclemlr  15448  ivthinclemuopn  15449  ivthinclemur  15450  ivthinclemloc  15452  ivthinc  15454  limcimolemlt  15475  limccnp2lem  15487  limccnp2cntop  15488  limccoap  15489  dvcj  15520  dvmptfsum  15536  dveflem  15537  plyf  15548  plyaddlem1  15558  plymullem1  15559  plycolemc  15569  plyco  15570  plycj  15572  dvply1  15576  dvply2g  15577  efltlemlt  15585  sin0pilem1  15592  sin0pilem2  15593  pilem3  15594  coseq0negpitopi  15647  abssinper  15657  cos02pilt1  15662  relogeftb  15676  logbgcd1irraplemexp  15779  logbgcd1irrap  15781  dvdsppwf1o  15803  mpodvdsmulf1o  15804  mersenne  15811  perfectlem2  15814  perfect  15815  lgsval  15823  lgsfvalg  15824  lgsfcl2  15825  lgsval2lem  15829  lgsmod  15845  lgsdilem  15846  lgsdir2lem4  15850  lgsdir2  15852  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem2  15901  2lgslem1a1  15905  2lgslem1a  15907  2sqlem5  15938  2sqlem6  15939  2sqlem7  15940  2sqlem9  15943  2sqlem10  15944  umgrnloopv  16055  uhgr2edg  16147  upgredginwlk  16297  clwwlkccatlem  16341  eupth2lem3lem3fi  16411  eupth2lem3lem4fi  16414  eupth2lemsfi  16419  depindlem3  16449  bj-findis  16695  2omap  16715  pwle2  16720  pwf1oexmid  16721  pw1nct  16725  nnsf  16731  peano4nninf  16732  nninfall  16735  nninfsellemeq  16740  nninfsellemeqinf  16742  nnnninfex  16748  nninfnfiinf  16749  qdencn  16755  refeq  16756  trilpolemeq1  16772  trilpolemlt1  16773  trirec0  16776  nconstwlpolemgt0  16797  nconstwlpolem  16798  neapmkvlem  16800  gfsumval  16809  gfsumcl  16816