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  vtoclgft  2789  reupick  3421  euotd  4256  frirrg  4352  ralxfrd  4464  nnsucpred  4618  foun  5482  f1oprg  5507  dffo4  5666  foeqcnvco  5793  fliftfun  5799  isotr  5819  riotass2  5859  ovmpodxf  6002  mpoxopoveq  6243  tfrlem1  6311  tfrlemibacc  6329  tfrlemibfn  6331  tfrlemi14d  6336  tfrexlem  6337  tfr1onlembacc  6345  tfr1onlembfn  6347  tfr1onlemres  6352  tfrcllembacc  6358  tfrcllembfn  6360  tfrcllemres  6365  frecabcl  6402  nnmordi  6519  eroprf  6630  f1imaen2g  6795  xpen  6847  mapen  6848  mapdom1g  6849  mapxpen  6850  xpmapenlem  6851  phplem4dom  6864  nndomo  6866  phpm  6867  fidifsnen  6872  dif1enen  6882  fisbth  6885  fimax2gtrilemstep  6902  fimax2gtri  6903  en2eqpr  6909  unsnfidcex  6921  unsnfidcel  6922  ssfirab  6935  fidcenumlemrks  6954  sbthlemi8  6965  fiuni  6979  ordiso2  7036  updjud  7083  difinfsnlem  7100  ctssdclemn0  7111  ctssdccl  7112  ctssdc  7114  enumctlemm  7115  enumct  7116  nnnninfeq  7128  nninfisol  7133  enomnilem  7138  fodju0  7147  enmkvlem  7161  enwomnilem  7169  nninfwlpoimlemg  7175  exmidfodomrlemim  7202  exmidontriimlem2  7223  exmidapne  7261  cc3  7269  dfplpq2  7355  nqpi  7379  nqnq0pi  7439  nq0nn  7443  elinp  7475  elnp1st2nd  7477  genprndl  7522  genprndu  7523  addnqprllem  7528  addnqprulem  7529  addnqprl  7530  addnqpru  7531  addlocpr  7537  nqprloc  7546  prmuloc  7567  mulnqprl  7569  mulnqpru  7570  mullocpr  7572  distrlem1prl  7583  distrlem1pru  7584  ltsopr  7597  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemloc  7608  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  aptiprleml  7640  aptiprlemu  7641  archpr  7644  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  cauappcvgprlemladdru  7657  archrecpr  7665  caucvgprlemnkj  7667  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemdisj  7675  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprprlemnkltj  7690  caucvgprprlemnkeqj  7691  caucvgprprlemnjltk  7692  caucvgprprlemml  7695  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemdisj  7703  caucvgprprlemexbt  7707  caucvgprprlemexb  7708  caucvgprprlemaddq  7709  suplocexprlemru  7720  suplocexprlemloc  7722  suplocexprlemex  7723  suplocexprlemub  7724  suplocexprlemlub  7725  mulgt0sr  7779  caucvgsrlemcau  7794  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  suplocsrlemb  7807  suplocsrlempr  7808  suplocsrlem  7809  axcaucvglemcau  7899  axcaucvglemres  7900  axpre-suploclemres  7902  axsuploc  8032  cnegexlem1  8134  cnegex  8137  apsym  8565  apcotr  8566  apadd1  8567  mulext1  8571  mulge0  8578  apti  8581  aprcl  8605  conjmulap  8688  lemulge11  8825  creui  8919  nndiv  8962  zaddcllemneg  9294  suprzclex  9353  eluzuzle  9538  infregelbex  9600  divfnzn  9623  qapne  9641  xrltso  9798  xnn0dcle  9804  xnn0letri  9805  xrre  9822  xrre3  9824  xaddf  9846  xaddval  9847  xpncan  9873  xleadd1a  9875  xltadd1  9878  xleaddadd  9889  ixxss12  9908  elioc2  9938  elico2  9939  elicc2  9940  fzm1  10102  fzneuz  10103  eluzgtdifelfzo  10199  elfzonelfzo  10232  exfzdc  10242  qtri3or  10245  exbtwnzlemstep  10250  exbtwnzlemex  10252  exbtwnz  10253  modqid  10351  modqcyc2  10362  modqmuladd  10368  modqmuladdnn0  10370  modaddmodlo  10390  addmodlteq  10400  frecuzrdgrrn  10410  frec2uzrdg  10411  frecuzrdgsuc  10416  frecuzrdgsuctlem  10425  seq3clss  10469  iseqf1olemqcl  10488  iseqf1olemnab  10490  iseqf1olemab  10491  iseqf1olemmo  10494  iseqf1olemqf1o  10495  iseqf1olemjpcl  10497  iseqf1olemqpcl  10498  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1olemp  10504  seq3f1oleml  10505  seq3f1o  10506  seq3id3  10509  ser3ge0  10519  exp3val  10524  expap0  10552  qsqeqor  10633  modqexp  10649  nn0ltexp2  10691  facndiv  10721  faclbnd  10723  bcval5  10745  hashunlem  10786  hashun  10787  hashprg  10790  fiprsshashgt1  10799  hashfacen  10818  zfz1isolemiso  10821  zfz1isolem1  10822  seq3coll  10824  ovshftex  10830  2shfti  10842  seq3shft  10849  cjap  10917  caucvgrelemcau  10991  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniq  11006  resqrexlemdecn  11023  resqrexlemcalc3  11027  resqrexlemcvg  11030  resqrexlemoverl  11032  leabs  11085  absexpzap  11091  ltabs  11098  abslt  11099  absle  11100  maxleim  11216  maxabslemval  11219  fimaxre2  11237  minmax  11240  2zinfmin  11253  xrmaxiflemcl  11255  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemcom  11259  xrmaxltsup  11268  xrmaxadd  11271  xrminmax  11275  xrbdtri  11286  2clim  11311  climshftlemg  11312  climsqz  11345  climsqz2  11346  climrecvg1n  11358  climcvg1nlem  11359  serf0  11362  sumrbdclem  11387  fsum3cvg  11388  summodclem3  11390  summodclem2a  11391  summodclem2  11392  zsumdc  11394  fsum3  11397  isumss  11401  fisumss  11402  fsum3cvg3  11406  fsumcl2lem  11408  fsumadd  11416  fsumsplit  11417  sumsnf  11419  fsum2d  11445  fisum0diag2  11457  fsummulc2  11458  modfsummod  11468  fsumabs  11475  fsumrelem  11481  fsumiun  11487  geoisumr  11528  cvgratnnlemseq  11536  cvgratz  11542  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodrbdclem  11581  fproddccvg  11582  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodntrivap  11594  fprodssdc  11600  fprodmul  11601  prodsnf  11602  fprodsplitdc  11606  fprodsplit  11607  fprodunsn  11614  fprodcl2lem  11615  fprodap0  11631  fprod2d  11633  fprodrec  11639  fprodap0f  11646  efcj  11683  efaddlem  11684  tanaddaplem  11748  nndivides  11806  dvdsext  11863  divalglemeunn  11928  divalglemex  11929  divalglemeuneg  11930  zsupcllemstep  11948  infssuzex  11952  suprzubdc  11955  nninfdcex  11956  zsupssdc  11957  dvdsbnd  11959  bezoutlemnewy  11999  bezoutlemstep  12000  bezoutlemmain  12001  bezoutlemzz  12005  bezoutlemaz  12006  bezoutlembz  12007  bezoutlemeu  12010  bezoutlemle  12011  bezoutlemsup  12012  dfgcd3  12013  dfgcd2  12017  bezoutr1  12036  nnmindc  12037  dvdslcm  12071  lcmgcdlem  12079  qredeq  12098  qredeu  12099  divgcdcoprm0  12103  divgcdcoprmex  12104  cncongr1  12105  isprm2lem  12118  prmind2  12122  exprmfct  12140  prmdvdsfz  12141  isprm5lem  12143  prmexpb  12153  rpexp1i  12156  sqrt2irr  12164  sqne2sq  12179  nonsq  12209  phiprmpw  12224  eulerthlemrprm  12231  eulerthlema  12232  hashgcdeq  12241  phisum  12242  modprmn0modprm0  12258  pclemub  12289  pclemdc  12290  pcmul  12303  pcqmul  12305  pcdvdstr  12328  pcprmpw2  12334  difsqpwdvds  12339  pcmpt  12343  oddprmdvds  12354  prmpwdvds  12355  pockthg  12357  infpnlem1  12359  1arith  12367  4sqlem2  12389  ennnfonelemg  12406  ennnfoneleminc  12414  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemfun  12420  ennnfonelemf1  12421  ennnfonelemrn  12422  ennnfonelemdm  12423  ennnfonelemnn0  12425  ennnfonelemim  12427  exmidunben  12429  ctinfomlemom  12430  ctinf  12433  ctiunctlemudc  12440  nninfdclemlt  12454  nninfdclemf1  12455  isstruct2r  12475  imasival  12732  mndpropd  12846  issubmnd  12848  mndissubm  12871  mhmeql  12881  grpinvnz  12946  mhmmnd  12985  mulgfng  12992  mulgz  13016  mulgnndir  13017  mulgnn0dir  13018  mulgneg2  13022  mulgass  13025  mhmmulg  13029  issubgrpd2  13055  issubg4m  13058  grpissubg  13059  isnsg3  13072  issrg  13153  ringpropd  13222  ringinvnz1ne0  13231  dvdsrvald  13267  dvdsrd  13268  dvdsrtr  13275  unitgrp  13290  lmodfopne  13421  lmodprop2d  13443  lssvacl  13466  lsslss  13473  lss1d  13475  tgdom  13611  neipsm  13693  tgrest  13708  cnfval  13733  cnpfval  13734  cnpval  13737  iscnp4  13757  cnpnei  13758  cnptopco  13761  cncnpi  13767  cncnp  13769  cnptopresti  13777  cnptoprest2  13779  cndis  13780  lmtopcnp  13789  txbasval  13806  neitx  13807  txcnp  13810  txcnmpt  13812  txcn  13814  imasnopn  13838  psmetres2  13872  isxmet2d  13887  xblss2ps  13943  xblss2  13944  blbas  13972  neibl  14030  metss2lem  14036  metrest  14045  xmettx  14049  metcnp3  14050  metcnp  14051  metcnp2  14052  metcnpi  14054  metcnpi2  14055  mulc1cncf  14115  cncfco  14117  mulcncflem  14129  mulcncf  14130  dedekindeulemuub  14134  dedekindeulemloc  14136  dedekindeulemlu  14138  dedekindeu  14140  suplociccreex  14141  suplociccex  14142  dedekindicclemuub  14143  dedekindicclemloc  14145  dedekindicclemlu  14147  dedekindicclemicc  14149  dedekindicc  14150  ivthinclemlopn  14153  ivthinclemlr  14154  ivthinclemuopn  14155  ivthinclemur  14156  ivthinclemloc  14158  ivthinc  14160  limcimolemlt  14172  limccnp2lem  14184  limccnp2cntop  14185  limccoap  14186  dvcj  14212  dveflem  14226  efltlemlt  14234  sin0pilem1  14241  sin0pilem2  14242  pilem3  14243  coseq0negpitopi  14296  abssinper  14306  cos02pilt1  14311  relogeftb  14325  logbgcd1irraplemexp  14425  logbgcd1irrap  14427  lgsval  14444  lgsfvalg  14445  lgsfcl2  14446  lgsval2lem  14450  lgsmod  14466  lgsdilem  14467  lgsdir2lem4  14471  lgsdir2  14473  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgsdirnn0  14487  lgsdinn0  14488  2sqlem5  14505  2sqlem6  14506  2sqlem7  14507  2sqlem9  14510  2sqlem10  14511  bj-findis  14770  pwle2  14787  pwf1oexmid  14788  pw1nct  14791  nnsf  14793  peano4nninf  14794  nninfall  14797  nninfsellemeq  14802  nninfsellemeqinf  14804  qdencn  14814  refeq  14815  trilpolemeq1  14827  trilpolemlt1  14828  trirec0  14831  nconstwlpolemgt0  14851  nconstwlpolem  14852  neapmkvlem  14854