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  2802  reupick  3434  euotd  4272  frirrg  4368  ralxfrd  4480  nnsucpred  4634  foun  5499  f1oprg  5524  dffo4  5685  foeqcnvco  5812  fliftfun  5818  isotr  5838  riotass2  5878  ovmpodxf  6022  mpoxopoveq  6265  tfrlem1  6333  tfrlemibacc  6351  tfrlemibfn  6353  tfrlemi14d  6358  tfrexlem  6359  tfr1onlembacc  6367  tfr1onlembfn  6369  tfr1onlemres  6374  tfrcllembacc  6380  tfrcllembfn  6382  tfrcllemres  6387  frecabcl  6424  nnmordi  6541  eroprf  6654  f1imaen2g  6819  pw2f1odclem  6862  xpen  6873  mapen  6874  mapdom1g  6875  mapxpen  6876  xpmapenlem  6877  phplem4dom  6890  nndomo  6892  phpm  6893  fidifsnen  6898  dif1enen  6908  fisbth  6911  fimax2gtrilemstep  6928  fimax2gtri  6929  en2eqpr  6935  unsnfidcex  6948  unsnfidcel  6949  ssfirab  6962  fidcenumlemrks  6982  sbthlemi8  6993  fiuni  7007  ordiso2  7064  updjud  7111  difinfsnlem  7128  ctssdclemn0  7139  ctssdccl  7140  ctssdc  7142  enumctlemm  7143  enumct  7144  nnnninfeq  7156  nninfisol  7161  enomnilem  7166  fodju0  7175  enmkvlem  7189  enwomnilem  7197  nninfwlpoimlemg  7203  exmidfodomrlemim  7230  exmidontriimlem2  7251  exmidapne  7289  cc3  7297  dfplpq2  7383  nqpi  7407  nqnq0pi  7467  nq0nn  7471  elinp  7503  elnp1st2nd  7505  genprndl  7550  genprndu  7551  addnqprllem  7556  addnqprulem  7557  addnqprl  7558  addnqpru  7559  addlocpr  7565  nqprloc  7574  prmuloc  7595  mulnqprl  7597  mulnqpru  7598  mullocpr  7600  distrlem1prl  7611  distrlem1pru  7612  ltsopr  7625  ltexprlemopl  7630  ltexprlemopu  7632  ltexprlemloc  7636  ltexprlemrl  7639  ltexprlemru  7641  addcanprleml  7643  addcanprlemu  7644  recexprlemloc  7660  recexprlem1ssl  7662  recexprlem1ssu  7663  aptiprleml  7668  aptiprlemu  7669  archpr  7672  cauappcvgprlemm  7674  cauappcvgprlemopl  7675  cauappcvgprlemlol  7676  cauappcvgprlemladdfu  7683  cauappcvgprlemladdfl  7684  cauappcvgprlemladdru  7685  archrecpr  7693  caucvgprlemnkj  7695  caucvgprlemm  7697  caucvgprlemopl  7698  caucvgprlemlol  7699  caucvgprlemdisj  7703  caucvgprlemloc  7704  caucvgprlemladdfu  7706  caucvgprprlemnkltj  7718  caucvgprprlemnkeqj  7719  caucvgprprlemnjltk  7720  caucvgprprlemml  7723  caucvgprprlemopl  7726  caucvgprprlemlol  7727  caucvgprprlemdisj  7731  caucvgprprlemexbt  7735  caucvgprprlemexb  7736  caucvgprprlemaddq  7737  suplocexprlemru  7748  suplocexprlemloc  7750  suplocexprlemex  7751  suplocexprlemub  7752  suplocexprlemlub  7753  mulgt0sr  7807  caucvgsrlemcau  7822  caucvgsrlemoffcau  7827  caucvgsrlemoffres  7829  suplocsrlemb  7835  suplocsrlempr  7836  suplocsrlem  7837  axcaucvglemcau  7927  axcaucvglemres  7928  axpre-suploclemres  7930  axsuploc  8060  cnegexlem1  8162  cnegex  8165  apsym  8593  apcotr  8594  apadd1  8595  mulext1  8599  mulge0  8606  apti  8609  aprcl  8633  conjmulap  8716  lemulge11  8853  creui  8947  nndiv  8990  zaddcllemneg  9322  suprzclex  9381  eluzuzle  9566  infregelbex  9628  divfnzn  9651  qapne  9669  xrltso  9826  xnn0dcle  9832  xnn0letri  9833  xrre  9850  xrre3  9852  xaddf  9874  xaddval  9875  xpncan  9901  xleadd1a  9903  xltadd1  9906  xleaddadd  9917  ixxss12  9936  elioc2  9966  elico2  9967  elicc2  9968  fzm1  10130  fzneuz  10131  eluzgtdifelfzo  10227  elfzonelfzo  10260  exfzdc  10270  qtri3or  10273  exbtwnzlemstep  10278  exbtwnzlemex  10280  exbtwnz  10281  modqid  10380  modqcyc2  10391  modqmuladd  10397  modqmuladdnn0  10399  modaddmodlo  10419  addmodlteq  10429  frecuzrdgrrn  10439  frec2uzrdg  10440  frecuzrdgsuc  10445  frecuzrdgsuctlem  10454  seq3clss  10498  iseqf1olemqcl  10517  iseqf1olemnab  10519  iseqf1olemab  10520  iseqf1olemmo  10523  iseqf1olemqf1o  10524  iseqf1olemjpcl  10526  iseqf1olemqpcl  10527  seq3f1olemqsumk  10530  seq3f1olemqsum  10531  seq3f1olemp  10533  seq3f1oleml  10534  seq3f1o  10535  seq3id3  10538  ser3ge0  10548  exp3val  10553  expap0  10581  qsqeqor  10662  modqexp  10678  nn0ltexp2  10721  facndiv  10751  faclbnd  10753  bcval5  10775  hashunlem  10816  hashun  10817  hashprg  10820  fiprsshashgt1  10829  hashfacen  10848  zfz1isolemiso  10851  zfz1isolem1  10852  seq3coll  10854  ovshftex  10860  2shfti  10872  seq3shft  10879  cjap  10947  caucvgrelemcau  11021  cvg1nlemcau  11025  cvg1nlemres  11026  recvguniq  11036  resqrexlemdecn  11053  resqrexlemcalc3  11057  resqrexlemcvg  11060  resqrexlemoverl  11062  leabs  11115  absexpzap  11121  ltabs  11128  abslt  11129  absle  11130  maxleim  11246  maxabslemval  11249  fimaxre2  11267  minmax  11270  2zinfmin  11283  xrmaxiflemcl  11285  xrmaxifle  11286  xrmaxiflemab  11287  xrmaxiflemlub  11288  xrmaxiflemcom  11289  xrmaxltsup  11298  xrmaxadd  11301  xrminmax  11305  xrbdtri  11316  2clim  11341  climshftlemg  11342  climsqz  11375  climsqz2  11376  climrecvg1n  11388  climcvg1nlem  11389  serf0  11392  sumrbdclem  11417  fsum3cvg  11418  summodclem3  11420  summodclem2a  11421  summodclem2  11422  zsumdc  11424  fsum3  11427  isumss  11431  fisumss  11432  fsum3cvg3  11436  fsumcl2lem  11438  fsumadd  11446  fsumsplit  11447  sumsnf  11449  fsum2d  11475  fisum0diag2  11487  fsummulc2  11488  modfsummod  11498  fsumabs  11505  fsumrelem  11511  fsumiun  11517  geoisumr  11558  cvgratnnlemseq  11566  cvgratz  11572  mertenslemi1  11575  mertenslem2  11576  mertensabs  11577  prodrbdclem  11611  fproddccvg  11612  prodmodclem3  11615  prodmodclem2a  11616  zproddc  11619  fprodseq  11623  fprodntrivap  11624  fprodssdc  11630  fprodmul  11631  prodsnf  11632  fprodsplitdc  11636  fprodsplit  11637  fprodunsn  11644  fprodcl2lem  11645  fprodap0  11661  fprod2d  11663  fprodrec  11669  fprodap0f  11676  efcj  11713  efaddlem  11714  tanaddaplem  11778  nndivides  11836  dvdsext  11893  divalglemeunn  11958  divalglemex  11959  divalglemeuneg  11960  zsupcllemstep  11978  infssuzex  11982  suprzubdc  11985  nninfdcex  11986  zsupssdc  11987  dvdsbnd  11989  bezoutlemnewy  12029  bezoutlemstep  12030  bezoutlemmain  12031  bezoutlemzz  12035  bezoutlemaz  12036  bezoutlembz  12037  bezoutlemeu  12040  bezoutlemle  12041  bezoutlemsup  12042  dfgcd3  12043  dfgcd2  12047  bezoutr1  12066  nnmindc  12067  dvdslcm  12101  lcmgcdlem  12109  qredeq  12128  qredeu  12129  divgcdcoprm0  12133  divgcdcoprmex  12134  cncongr1  12135  isprm2lem  12148  prmind2  12152  exprmfct  12170  prmdvdsfz  12171  isprm5lem  12173  prmexpb  12183  rpexp1i  12186  sqrt2irr  12194  sqne2sq  12209  nonsq  12239  phiprmpw  12254  eulerthlemrprm  12261  eulerthlema  12262  hashgcdeq  12271  phisum  12272  modprmn0modprm0  12288  pclemub  12319  pclemdc  12320  pcmul  12333  pcqmul  12335  pcxqcl  12344  pcdvdstr  12359  pcprmpw2  12365  difsqpwdvds  12370  pcmpt  12375  oddprmdvds  12386  prmpwdvds  12387  pockthg  12389  infpnlem1  12391  1arith  12399  4sqlem2  12421  4sqlemafi  12427  4sqlemffi  12428  4sqleminfi  12429  4sqlem11  12433  4sqlem13m  12435  4sqlem14  12436  4sqlem17  12439  4sqlem18  12440  ennnfonelemg  12454  ennnfoneleminc  12462  ennnfonelemkh  12463  ennnfonelemhf1o  12464  ennnfonelemex  12465  ennnfonelemhom  12466  ennnfonelemfun  12468  ennnfonelemf1  12469  ennnfonelemrn  12470  ennnfonelemdm  12471  ennnfonelemnn0  12473  ennnfonelemim  12475  exmidunben  12477  ctinfomlemom  12478  ctinf  12481  ctiunctlemudc  12488  nninfdclemlt  12502  nninfdclemf1  12503  isstruct2r  12523  imasival  12783  sgrppropd  12876  mndpropd  12901  issubmnd  12903  mndissubm  12927  resmhm2b  12941  mhmeql  12944  grpinvnz  13015  mhmmnd  13058  mulgfng  13066  mulgz  13090  mulgnndir  13091  mulgnn0dir  13092  mulgneg2  13096  mulgass  13099  mhmmulg  13103  issubgrpd2  13129  issubg4m  13132  grpissubg  13133  isnsg3  13146  ghmpreima  13205  ghmnsgpreima  13208  ghmf1  13212  conjnmz  13218  conjnmzb  13219  eqgabl  13267  rngpropd  13309  issrg  13319  ringpropd  13392  ringinvnz1ne0  13401  dvdsrvald  13443  dvdsrd  13444  dvdsrtr  13451  unitgrp  13466  rhmopp  13526  lmodfopne  13642  lmodprop2d  13664  lssvacl  13681  lsslss  13697  lss1d  13699  lsspropdg  13747  rnglidlmcl  13796  lidlacl  13800  isridl  13819  psrval  13944  tgdom  14032  neipsm  14114  tgrest  14129  cnfval  14154  cnpfval  14155  cnpval  14158  iscnp4  14178  cnpnei  14179  cnptopco  14182  cncnpi  14188  cncnp  14190  cnptopresti  14198  cnptoprest2  14200  cndis  14201  lmtopcnp  14210  txbasval  14227  neitx  14228  txcnp  14231  txcnmpt  14233  txcn  14235  imasnopn  14259  psmetres2  14293  isxmet2d  14308  xblss2ps  14364  xblss2  14365  blbas  14393  neibl  14451  metss2lem  14457  metrest  14466  xmettx  14470  metcnp3  14471  metcnp  14472  metcnp2  14473  metcnpi  14475  metcnpi2  14476  mulc1cncf  14536  cncfco  14538  mulcncflem  14550  mulcncf  14551  dedekindeulemuub  14555  dedekindeulemloc  14557  dedekindeulemlu  14559  dedekindeu  14561  suplociccreex  14562  suplociccex  14563  dedekindicclemuub  14564  dedekindicclemloc  14566  dedekindicclemlu  14568  dedekindicclemicc  14570  dedekindicc  14571  ivthinclemlopn  14574  ivthinclemlr  14575  ivthinclemuopn  14576  ivthinclemur  14577  ivthinclemloc  14579  ivthinc  14581  limcimolemlt  14593  limccnp2lem  14605  limccnp2cntop  14606  limccoap  14607  dvcj  14633  dveflem  14647  efltlemlt  14655  sin0pilem1  14662  sin0pilem2  14663  pilem3  14664  coseq0negpitopi  14717  abssinper  14727  cos02pilt1  14732  relogeftb  14746  logbgcd1irraplemexp  14846  logbgcd1irrap  14848  lgsval  14866  lgsfvalg  14867  lgsfcl2  14868  lgsval2lem  14872  lgsmod  14888  lgsdilem  14889  lgsdir2lem4  14893  lgsdir2  14895  lgsdir  14897  lgsdilem2  14898  lgsdi  14899  lgsne0  14900  lgsdirnn0  14909  lgsdinn0  14910  2sqlem5  14927  2sqlem6  14928  2sqlem7  14929  2sqlem9  14932  2sqlem10  14933  bj-findis  15192  pwle2  15210  pwf1oexmid  15211  pw1nct  15214  nnsf  15216  peano4nninf  15217  nninfall  15220  nninfsellemeq  15225  nninfsellemeqinf  15227  qdencn  15237  refeq  15238  trilpolemeq1  15250  trilpolemlt1  15251  trirec0  15254  nconstwlpolemgt0  15274  nconstwlpolem  15275  neapmkvlem  15277