Theorem ad2antrr 485

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 274	. 2 |- ( ( ph /\ th ) -> ps )
3	2	adantlr 474	1 |- ( ( ( ph /\ ch ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad3antrrr  489  ad5ant13  516  ad5ant23  519  simpll  524  simplll  528  simpllr  529  vtoclgft  2780  reupick  3411  euotd  4239  frirrg  4335  ralxfrd  4447  nnsucpred  4601  foun  5461  f1oprg  5486  dffo4  5644  foeqcnvco  5769  fliftfun  5775  isotr  5795  riotass2  5835  ovmpodxf  5978  mpoxopoveq  6219  tfrlem1  6287  tfrlemibacc  6305  tfrlemibfn  6307  tfrlemi14d  6312  tfrexlem  6313  tfr1onlembacc  6321  tfr1onlembfn  6323  tfr1onlemres  6328  tfrcllembacc  6334  tfrcllembfn  6336  tfrcllemres  6341  frecabcl  6378  nnmordi  6495  eroprf  6606  f1imaen2g  6771  xpen  6823  mapen  6824  mapdom1g  6825  mapxpen  6826  xpmapenlem  6827  phplem4dom  6840  nndomo  6842  phpm  6843  fidifsnen  6848  dif1enen  6858  fisbth  6861  fimax2gtrilemstep  6878  fimax2gtri  6879  en2eqpr  6885  unsnfidcex  6897  unsnfidcel  6898  ssfirab  6911  fidcenumlemrks  6930  sbthlemi8  6941  fiuni  6955  ordiso2  7012  updjud  7059  difinfsnlem  7076  ctssdclemn0  7087  ctssdccl  7088  ctssdc  7090  enumctlemm  7091  enumct  7092  nnnninfeq  7104  nninfisol  7109  enomnilem  7114  fodju0  7123  enmkvlem  7137  enwomnilem  7145  nninfwlpoimlemg  7151  exmidfodomrlemim  7178  exmidontriimlem2  7199  cc3  7230  dfplpq2  7316  nqpi  7340  nqnq0pi  7400  nq0nn  7404  elinp  7436  elnp1st2nd  7438  genprndl  7483  genprndu  7484  addnqprllem  7489  addnqprulem  7490  addnqprl  7491  addnqpru  7492  addlocpr  7498  nqprloc  7507  prmuloc  7528  mulnqprl  7530  mulnqpru  7531  mullocpr  7533  distrlem1prl  7544  distrlem1pru  7545  ltsopr  7558  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  aptiprleml  7601  aptiprlemu  7602  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  archrecpr  7626  caucvgprlemnkj  7628  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemdisj  7664  caucvgprprlemexbt  7668  caucvgprprlemexb  7669  caucvgprprlemaddq  7670  suplocexprlemru  7681  suplocexprlemloc  7683  suplocexprlemex  7684  suplocexprlemub  7685  suplocexprlemlub  7686  mulgt0sr  7740  caucvgsrlemcau  7755  caucvgsrlemoffcau  7760  caucvgsrlemoffres  7762  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axcaucvglemcau  7860  axcaucvglemres  7861  axpre-suploclemres  7863  axsuploc  7992  cnegexlem1  8094  cnegex  8097  apsym  8525  apcotr  8526  apadd1  8527  mulext1  8531  mulge0  8538  apti  8541  aprcl  8565  conjmulap  8646  lemulge11  8782  creui  8876  nndiv  8919  zaddcllemneg  9251  suprzclex  9310  eluzuzle  9495  infregelbex  9557  divfnzn  9580  qapne  9598  xrltso  9753  xnn0dcle  9759  xnn0letri  9760  xrre  9777  xrre3  9779  xaddf  9801  xaddval  9802  xpncan  9828  xleadd1a  9830  xltadd1  9833  xleaddadd  9844  ixxss12  9863  elioc2  9893  elico2  9894  elicc2  9895  fzm1  10056  fzneuz  10057  eluzgtdifelfzo  10153  elfzonelfzo  10186  exfzdc  10196  qtri3or  10199  exbtwnzlemstep  10204  exbtwnzlemex  10206  exbtwnz  10207  modqid  10305  modqcyc2  10316  modqmuladd  10322  modqmuladdnn0  10324  modaddmodlo  10344  addmodlteq  10354  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgsuc  10370  frecuzrdgsuctlem  10379  seq3clss  10423  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemmo  10448  iseqf1olemqf1o  10449  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemp  10458  seq3f1oleml  10459  seq3f1o  10460  seq3id3  10463  ser3ge0  10473  exp3val  10478  expap0  10506  qsqeqor  10586  modqexp  10602  nn0ltexp2  10644  facndiv  10673  faclbnd  10675  bcval5  10697  hashunlem  10739  hashun  10740  hashprg  10743  fiprsshashgt1  10752  hashfacen  10771  zfz1isolemiso  10774  zfz1isolem1  10775  seq3coll  10777  ovshftex  10783  2shfti  10795  seq3shft  10802  cjap  10870  caucvgrelemcau  10944  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniq  10959  resqrexlemdecn  10976  resqrexlemcalc3  10980  resqrexlemcvg  10983  resqrexlemoverl  10985  leabs  11038  absexpzap  11044  ltabs  11051  abslt  11052  absle  11053  maxleim  11169  maxabslemval  11172  fimaxre2  11190  minmax  11193  2zinfmin  11206  xrmaxiflemcl  11208  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemcom  11212  xrmaxltsup  11221  xrmaxadd  11224  xrminmax  11228  xrbdtri  11239  2clim  11264  climshftlemg  11265  climsqz  11298  climsqz2  11299  climrecvg1n  11311  climcvg1nlem  11312  serf0  11315  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  summodclem2  11345  zsumdc  11347  fsum3  11350  isumss  11354  fisumss  11355  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  fsumsplit  11370  sumsnf  11372  fsum2d  11398  fisum0diag2  11410  fsummulc2  11411  modfsummod  11421  fsumabs  11428  fsumrelem  11434  fsumiun  11440  geoisumr  11481  cvgratnnlemseq  11489  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodrbdclem  11534  fproddccvg  11535  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodntrivap  11547  fprodssdc  11553  fprodmul  11554  prodsnf  11555  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  fprodcl2lem  11568  fprodap0  11584  fprod2d  11586  fprodrec  11592  fprodap0f  11599  efcj  11636  efaddlem  11637  tanaddaplem  11701  nndivides  11759  dvdsext  11815  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  nninfdcex  11908  zsupssdc  11909  dvdsbnd  11911  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemzz  11957  bezoutlemaz  11958  bezoutlembz  11959  bezoutlemeu  11962  bezoutlemle  11963  bezoutlemsup  11964  dfgcd3  11965  dfgcd2  11969  bezoutr1  11988  nnmindc  11989  dvdslcm  12023  lcmgcdlem  12031  qredeq  12050  qredeu  12051  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  isprm2lem  12070  prmind2  12074  exprmfct  12092  prmdvdsfz  12093  isprm5lem  12095  prmexpb  12105  rpexp1i  12108  sqrt2irr  12116  sqne2sq  12131  nonsq  12161  phiprmpw  12176  eulerthlemrprm  12183  eulerthlema  12184  hashgcdeq  12193  phisum  12194  modprmn0modprm0  12210  pclemub  12241  pclemdc  12242  pcmul  12255  pcqmul  12257  pcdvdstr  12280  pcprmpw2  12286  difsqpwdvds  12291  pcmpt  12295  oddprmdvds  12306  prmpwdvds  12307  pockthg  12309  infpnlem1  12311  1arith  12319  4sqlem2  12341  ennnfonelemg  12358  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemfun  12372  ennnfonelemf1  12373  ennnfonelemrn  12374  ennnfonelemdm  12375  ennnfonelemnn0  12377  ennnfonelemim  12379  exmidunben  12381  ctinfomlemom  12382  ctinf  12385  ctiunctlemudc  12392  nninfdclemlt  12406  nninfdclemf1  12407  isstruct2r  12427  mndpropd  12676  mndissubm  12697  mhmeql  12707  grpinvnz  12770  tgdom  12866  neipsm  12948  tgrest  12963  cnfval  12988  cnpfval  12989  cnpval  12992  iscnp4  13012  cnpnei  13013  cnptopco  13016  cncnpi  13022  cncnp  13024  cnptopresti  13032  cnptoprest2  13034  cndis  13035  lmtopcnp  13044  txbasval  13061  neitx  13062  txcnp  13065  txcnmpt  13067  txcn  13069  imasnopn  13093  psmetres2  13127  isxmet2d  13142  xblss2ps  13198  xblss2  13199  blbas  13227  neibl  13285  metss2lem  13291  metrest  13300  xmettx  13304  metcnp3  13305  metcnp  13306  metcnp2  13307  metcnpi  13309  metcnpi2  13310  mulc1cncf  13370  cncfco  13372  mulcncflem  13384  mulcncf  13385  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeu  13395  suplociccreex  13396  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemicc  13404  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  ivthinc  13415  limcimolemlt  13427  limccnp2lem  13439  limccnp2cntop  13440  limccoap  13441  dvcj  13467  dveflem  13481  efltlemlt  13489  sin0pilem1  13496  sin0pilem2  13497  pilem3  13498  coseq0negpitopi  13551  abssinper  13561  cos02pilt1  13566  relogeftb  13580  logbgcd1irraplemexp  13680  logbgcd1irrap  13682  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsval2lem  13705  lgsmod  13721  lgsdilem  13722  lgsdir2lem4  13726  lgsdir2  13728  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  2sqlem5  13749  2sqlem6  13750  2sqlem7  13751  2sqlem9  13754  2sqlem10  13755  bj-findis  14014  pwle2  14031  pwf1oexmid  14032  pw1nct  14036  nnsf  14038  peano4nninf  14039  nninfall  14042  nninfsellemeq  14047  nninfsellemeqinf  14049  qdencn  14059  refeq  14060  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  nconstwlpolemgt0  14095  nconstwlpolem  14096  neapmkvlem  14098