Theorem ad2antrr 492

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 481	1 |- ( ( ( ph /\ ch ) /\ 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:  ad3antrrr  496  ad5ant13  523  ad5ant23  526  simpll  531  simplll  539  simpllr  540  ad5ant123  1270  vtoclgft  2873  reupick  3517  ifeqeqxdc  3687  euotd  4397  frirrg  4497  ralxfrd  4610  nnsucpred  4766  foun  5661  f1oprg  5688  dffo4  5859  funopsn  5894  foeqcnvco  5999  fliftfun  6005  isotr  6025  riotass2  6070  ovmpodxf  6217  suppfnss  6501  suppcofn  6510  mpoxopoveq  6516  tfrlem1  6584  tfrlemibacc  6602  tfrlemibfn  6604  tfrlemi14d  6609  tfrexlem  6610  tfr1onlembacc  6618  tfr1onlembfn  6620  tfr1onlemres  6625  tfrcllembacc  6631  tfrcllembfn  6633  tfrcllemres  6638  frecabcl  6675  nnmordi  6794  eroprf  6907  mapsnd  6976  f1imaen2g  7086  pw2f1odclem  7140  xpen  7151  mapen  7152  mapdom1g  7153  mapxpen  7154  xpmapenlem  7155  phplem4dom  7169  nndomo  7171  phpm  7173  fidifsnen  7178  dif1enen  7190  fisbth  7193  fimax2gtrilemstep  7211  fimax2gtri  7212  eqsndc  7216  en2eqpr  7220  unsnfidcex  7233  unsnfidcel  7234  ssfirab  7250  fidcenumlemrks  7277  sbthlemi8  7288  funisfsuppdc  7298  fiuni  7317  2omap  7324  ordiso2  7381  updjud  7428  difinfsnlem  7445  ctssdclemn0  7456  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  enumct  7461  nnnninfeq  7474  nninfisol  7479  enomnilem  7484  fodju0  7493  enmkvlem  7507  enwomnilem  7515  nninfwlpoimlemg  7521  pr1or2  7546  pr2cv1  7547  exmidfodomrlemim  7559  exmidontriimlem2  7584  exmidapne  7632  cc3  7640  dfplpq2  7727  nqpi  7751  nqnq0pi  7811  nq0nn  7815  elinp  7847  elnp1st2nd  7849  genprndl  7894  genprndu  7895  addnqprllem  7900  addnqprulem  7901  addnqprl  7902  addnqpru  7903  addlocpr  7909  nqprloc  7918  prmuloc  7939  mulnqprl  7941  mulnqpru  7942  mullocpr  7944  distrlem1prl  7955  distrlem1pru  7956  ltsopr  7969  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  archrecpr  8037  caucvgprlemnkj  8039  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemnjltk  8064  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemdisj  8075  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  caucvgprprlemaddq  8081  suplocexprlemru  8092  suplocexprlemloc  8094  suplocexprlemex  8095  suplocexprlemub  8096  suplocexprlemlub  8097  mulgt0sr  8151  caucvgsrlemcau  8166  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axcaucvglemcau  8271  axcaucvglemres  8272  axpre-suploclemres  8274  axsuploc  8404  cnegexlem1  8508  cnegex  8511  apsym  8942  apcotr  8943  apadd1  8944  mulext1  8948  mulge0  8955  apti  8958  aprcl  8982  conjmulap  9067  lemulge11  9204  creui  9298  nndiv  9354  zaddcllemneg  9692  suprzclex  9754  eluzuzle  9945  infregelbex  10013  divfnzn  10036  qapne  10054  xrltso  10214  xnn0dcle  10220  xnn0letri  10221  xrre  10238  xrre3  10240  xaddf  10262  xaddval  10263  xpncan  10289  xleadd1a  10291  xltadd1  10294  xleaddadd  10305  ixxss12  10324  elioc2  10354  elico2  10355  elicc2  10356  fzm1  10523  fzneuz  10524  eluzgtdifelfzo  10631  elfzonelfzo  10664  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  suprzubdc  10687  nninfdcex  10688  zsupssdc  10689  qtri3or  10691  exbtwnzlemstep  10698  exbtwnzlemex  10700  exbtwnz  10701  flaplt  10738  modqid  10806  modqcyc2  10817  modqmuladd  10823  modqmuladdnn0  10825  modaddmodlo  10845  addmodlteq  10855  frecuzrdgrrn  10865  frec2uzrdg  10866  frecuzrdgsuc  10871  frecuzrdgsuctlem  10880  nninfinf  10900  seq3clss  10928  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemmo  10962  iseqf1olemqf1o  10963  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1olemp  10972  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem1  10976  seqf1oglem2  10977  seqf1og  10978  seq3id3  10981  seqfeq4g  10988  ser3ge0  10993  exp3val  10998  expap0  11026  qsqeqor  11107  modqexp  11124  nn0sqdc  11167  nn0ltexp2  11168  facndiv  11198  faclbnd  11200  bcval5  11222  hashunlem  11265  hashun  11266  hashprg  11270  fiprsshashgt1  11279  hashfacen  11305  hashf1lem1  11306  zfz1isolemiso  11312  zfz1isolem1  11313  seq3coll  11315  hashtpglem  11319  ccatcl  11382  ccatlen  11384  ccatvalfn  11390  ccatsymb  11391  ccatrn  11398  ccat2s1fstg  11437  swrdclg  11443  swrdspsleq  11460  pfxeq  11489  swrdswrd  11498  wrdind  11515  wrd2ind  11516  swrdccatin1  11518  swrdccatin2  11522  pfxccatin12  11526  pfxccat3  11527  swrdccat3b  11533  reuccatpfxs1  11540  ovshftex  11605  2shfti  11617  seq3shft  11624  cjap  11693  caucvgrelemcau  11767  cvg1nlemcau  11771  cvg1nlemres  11772  recvguniq  11782  resqrexlemdecn  11799  resqrexlemcalc3  11803  resqrexlemcvg  11806  resqrexlemoverl  11808  leabs  11861  absexpzap  11868  ltabs  11875  abslt  11876  absle  11877  maxleim  11993  maxabslemval  11996  fimaxre2  12015  fiidxsupcl  12017  minmax  12019  2zinfmin  12033  xrmaxiflemcl  12035  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemcom  12039  xrmaxltsup  12048  xrmaxadd  12051  xrminmax  12055  xrbdtri  12066  2clim  12091  climshftlemg  12092  climsqz  12125  climsqz2  12126  climrecvg1n  12138  climcvg1nlem  12139  serf0  12142  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  summodclem2  12173  zsumdc  12175  fsum3  12178  isumss  12182  fisumss  12183  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  fsumsplit  12198  sumsnf  12200  fsum2d  12226  fisum0diag2  12238  fsummulc2  12239  modfsummod  12249  fsumabs  12256  fsumrelem  12262  fsumiun  12268  geoisumr  12309  cvgratnnlemseq  12317  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  prodrbdclem  12362  fproddccvg  12363  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodntrivap  12375  fprodssdc  12381  fprodmul  12382  prodsnf  12383  fprodsplitdc  12387  fprodsplit  12388  fprodunsn  12395  fprodcl2lem  12396  fprodap0  12412  fprod2d  12414  fprodrec  12420  fprodap0f  12427  efcj  12464  efaddlem  12465  tanaddaplem  12529  sinltxirr  12552  nndivides  12588  dvdsext  12646  divalglemeunn  12712  divalglemex  12713  divalglemeuneg  12714  bitsfzolem  12745  bitsmod  12747  bitsinv1  12753  dvdsbnd  12757  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemzz  12803  bezoutlemaz  12804  bezoutlembz  12805  bezoutlemeu  12808  bezoutlemle  12809  bezoutlemsup  12810  dfgcd3  12811  dfgcd2  12815  bezoutr1  12834  nnmindc  12835  nninfctlemfo  12841  dvdslcm  12871  lcmgcdlem  12879  qredeq  12898  qredeu  12899  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  isprm2lem  12918  prmind2  12922  exprmfct  12941  prmdvdsfz  12942  isprm5lem  12944  prmexpb  12954  rpexp1i  12957  sqrt2irr  12965  pwbdvdslemn  12968  sqne2sq  12981  nonsq  13011  phiprmpw  13028  eulerthlemrprm  13035  eulerthlema  13036  hashgcdeq  13046  phisum  13047  modprmn0modprm0  13063  pclemub  13094  pclemdc  13095  pcmul  13108  pcqmul  13110  pcxqcl  13119  pcdvdstr  13134  pcprmpw2  13140  difsqpwdvds  13145  pcmpt  13150  oddprmdvds  13161  prmpwdvds  13162  pockthg  13164  infpnlem1  13166  1arith  13174  4sqlem2  13196  4sqlemafi  13202  4sqlemffi  13203  4sqleminfi  13204  4sqlem11  13208  4sqlem13m  13210  4sqlem14  13211  4sqlem17  13214  4sqlem18  13215  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemscl  13304  ballotfilemimin  13306  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsv  13310  ballotfilemsdom  13312  ballotfilemsima  13316  ennnfonelemg  13351  ennnfoneleminc  13359  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemfun  13365  ennnfonelemf1  13366  ennnfonelemrn  13367  ennnfonelemdm  13368  ennnfonelemnn0  13370  ennnfonelemim  13372  exmidunben  13374  ctinfomlemom  13375  ctinf  13378  ctiunctlemudc  13385  nninfdclemlt  13399  nninfdclemf1  13400  isstruct2r  13420  imasival  13685  sgrppropd  13786  mndpropd  13811  issubmnd  13813  mndissubm  13840  resmhm2b  13854  mhmeql  13857  gzsumwsubmcl  13859  gzsumwmhm  13861  gzsumcl  13862  grpinvnz  13934  mhmmnd  13977  mulgfng  13985  mulgz  14011  mulgnndir  14012  mulgnn0dir  14013  mulgneg2  14017  mulgass  14020  mhmmulg  14024  issubgrpd2  14051  issubg4m  14054  grpissubg  14055  isnsg3  14068  ghmpreima  14127  ghmnsgpreima  14130  ghmf1  14134  conjnmz  14140  conjnmzb  14141  cntrsubgnsg  14174  eqgabl  14223  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gsumvalfi  14241  gsumclfi  14248  gsumf1ofi  14249  gsummptfidmadd  14250  gsumsubmclfi  14252  gsummptfidmsplit  14253  gsumresfi  14262  gsum2dfilem2  14271  prdsval  14279  prdssgrpd  14297  prdsidlem  14299  prdsmndd  14300  pws0g  14319  pwssub  14322  rngpropd  14360  issrg  14375  ringpropd  14449  ringinvnz1ne0  14460  dvdsrvald  14508  dvdsrd  14509  dvdsrtr  14516  unitgrp  14531  rhmopp  14591  aprnzr  14707  opprdrng  14728  lmodfopne  14771  lmodprop2d  14793  lssvacl  14810  lsslss  14826  lss1d  14828  lsspropdg  14876  rnglidlmcl  14925  lidlacl  14929  isridl  14949  gsumfsum  15031  znidomb  15101  znunit  15102  znrrg  15103  issubassa2  15143  psrval  15160  psrbaglefifi  15175  psrbagmaxlem1  15178  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  psrbagmax  15183  rhmpsrfilem2  15194  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  mvrffi  15218  mplsubgfilemcl  15232  mplsubgfi  15234  tgdom  15315  neipsm  15397  tgrest  15412  cnfval  15437  cnpfval  15438  cnpval  15441  iscnp4  15461  cnpnei  15462  cnptopco  15465  cncnpi  15471  cncnp  15473  cnptopresti  15481  cnptoprest2  15483  cndis  15484  lmtopcnp  15493  txbasval  15510  neitx  15511  txcnp  15514  txcnmpt  15516  txcn  15518  imasnopn  15542  psmetres2  15576  isxmet2d  15591  xblss2ps  15647  xblss2  15648  blbas  15676  neibl  15734  metss2lem  15740  metrest  15749  xmettx  15753  metcnp3  15754  metcnp  15755  metcnp2  15756  metcnpi  15758  metcnpi2  15759  mulc1cncf  15832  cncfco  15834  mulcncflem  15850  mulcncf  15851  dedekindeulemuub  15860  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeu  15866  suplociccreex  15867  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicclemicc  15875  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthinc  15886  limcimolemlt  15907  limccnp2lem  15919  limccnp2cntop  15920  limccoap  15921  dvcj  15952  dvmptfsum  15968  dveflem  15969  plyf  15980  plyaddlem1  15990  plymullem1  15991  plycolemc  16001  plyco  16002  plycj  16004  dvply1  16008  dvply2g  16009  efltlemlt  16017  efap1p  16022  sin0pilem1  16025  sin0pilem2  16026  pilem3  16027  coseq0negpitopi  16080  abssinper  16090  cos02pilt1  16096  relogeftb  16111  logdivlt  16141  logbgcd1irraplemexp  16221  logbgcd1irrap  16223  birthdaylem2  16243  ppiqltx  16298  dvdsppwf1o  16300  mpodvdsmulf1o  16301  ppiqub  16310  chtqub  16313  mersenne  16314  perfectlem2  16317  perfect  16318  pcbcctr  16320  bposlem1  16328  bposlem3  16330  bposlem5  16332  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgsval2lem  16351  lgsmod  16367  lgsdilem  16368  lgsdir2lem4  16372  lgsdir2  16374  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem2  16423  2lgslem1a1  16427  2lgslem1a  16429  2sqlem5  16460  2sqlem6  16461  2sqlem7  16462  2sqlem9  16465  2sqlem10  16466  umgrnloopv  16577  uhgr2edg  16669  upgredginwlk  16819  clwwlkccatlem  16863  eupth2lem3lem3fi  16933  eupth2lem3lem4fi  16936  eupth2lemsfi  16941  depindlem3  16971  bj-findis  17227  pwle2  17250  pwf1oexmid  17251  pw1nct  17255  wexmiddiffi  17266  nnsf  17271  peano4nninf  17272  nninfall  17275  nninfsellemeq  17280  nninfsellemeqinf  17282  nnnninfex  17288  nninfnfiinf  17289  qdencn  17295  refeq  17296  trilpolemeq1  17313  trilpolemlt1  17314  trirec0  17317  nconstwlpolemgt0  17338  nconstwlpolem  17339  neapmkvlem  17341