Theorem ad2antrr 480

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 469	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  484  ad5ant13  511  ad5ant23  514  simpll  519  simplll  523  simpllr  524  vtoclgft  2776  reupick  3406  euotd  4232  frirrg  4328  ralxfrd  4440  nnsucpred  4594  foun  5451  f1oprg  5476  dffo4  5633  foeqcnvco  5758  fliftfun  5764  isotr  5784  riotass2  5824  ovmpodxf  5967  mpoxopoveq  6208  tfrlem1  6276  tfrlemibacc  6294  tfrlemibfn  6296  tfrlemi14d  6301  tfrexlem  6302  tfr1onlembacc  6310  tfr1onlembfn  6312  tfr1onlemres  6317  tfrcllembacc  6323  tfrcllembfn  6325  tfrcllemres  6330  frecabcl  6367  nnmordi  6484  eroprf  6594  f1imaen2g  6759  xpen  6811  mapen  6812  mapdom1g  6813  mapxpen  6814  xpmapenlem  6815  phplem4dom  6828  nndomo  6830  phpm  6831  fidifsnen  6836  dif1enen  6846  fisbth  6849  fimax2gtrilemstep  6866  fimax2gtri  6867  en2eqpr  6873  unsnfidcex  6885  unsnfidcel  6886  ssfirab  6899  fidcenumlemrks  6918  sbthlemi8  6929  fiuni  6943  ordiso2  7000  updjud  7047  difinfsnlem  7064  ctssdclemn0  7075  ctssdccl  7076  ctssdc  7078  enumctlemm  7079  enumct  7080  nnnninfeq  7092  nninfisol  7097  enomnilem  7102  fodju0  7111  enmkvlem  7125  enwomnilem  7133  exmidfodomrlemim  7157  exmidontriimlem2  7178  cc3  7209  dfplpq2  7295  nqpi  7319  nqnq0pi  7379  nq0nn  7383  elinp  7415  elnp1st2nd  7417  genprndl  7462  genprndu  7463  addnqprllem  7468  addnqprulem  7469  addnqprl  7470  addnqpru  7471  addlocpr  7477  nqprloc  7486  prmuloc  7507  mulnqprl  7509  mulnqpru  7510  mullocpr  7512  distrlem1prl  7523  distrlem1pru  7524  ltsopr  7537  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemloc  7548  ltexprlemrl  7551  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  recexprlemloc  7572  recexprlem1ssl  7574  recexprlem1ssu  7575  aptiprleml  7580  aptiprlemu  7581  archpr  7584  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  archrecpr  7605  caucvgprlemnkj  7607  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprprlemnkltj  7630  caucvgprprlemnkeqj  7631  caucvgprprlemnjltk  7632  caucvgprprlemml  7635  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemdisj  7643  caucvgprprlemexbt  7647  caucvgprprlemexb  7648  caucvgprprlemaddq  7649  suplocexprlemru  7660  suplocexprlemloc  7662  suplocexprlemex  7663  suplocexprlemub  7664  suplocexprlemlub  7665  mulgt0sr  7719  caucvgsrlemcau  7734  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  axcaucvglemcau  7839  axcaucvglemres  7840  axpre-suploclemres  7842  axsuploc  7971  cnegexlem1  8073  cnegex  8076  apsym  8504  apcotr  8505  apadd1  8506  mulext1  8510  mulge0  8517  apti  8520  aprcl  8544  conjmulap  8625  lemulge11  8761  creui  8855  nndiv  8898  zaddcllemneg  9230  suprzclex  9289  eluzuzle  9474  infregelbex  9536  divfnzn  9559  qapne  9577  xrltso  9732  xnn0dcle  9738  xnn0letri  9739  xrre  9756  xrre3  9758  xaddf  9780  xaddval  9781  xpncan  9807  xleadd1a  9809  xltadd1  9812  xleaddadd  9823  ixxss12  9842  elioc2  9872  elico2  9873  elicc2  9874  fzm1  10035  fzneuz  10036  eluzgtdifelfzo  10132  elfzonelfzo  10165  exfzdc  10175  qtri3or  10178  exbtwnzlemstep  10183  exbtwnzlemex  10185  exbtwnz  10186  modqid  10284  modqcyc2  10295  modqmuladd  10301  modqmuladdnn0  10303  modaddmodlo  10323  addmodlteq  10333  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgsuc  10349  frecuzrdgsuctlem  10358  seq3clss  10402  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemab  10424  iseqf1olemmo  10427  iseqf1olemqf1o  10428  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1olemp  10437  seq3f1oleml  10438  seq3f1o  10439  seq3id3  10442  ser3ge0  10452  exp3val  10457  expap0  10485  qsqeqor  10565  modqexp  10581  nn0ltexp2  10623  facndiv  10652  faclbnd  10654  bcval5  10676  hashunlem  10717  hashun  10718  hashprg  10721  fiprsshashgt1  10730  hashfacen  10749  zfz1isolemiso  10752  zfz1isolem1  10753  seq3coll  10755  ovshftex  10761  2shfti  10773  seq3shft  10780  cjap  10848  caucvgrelemcau  10922  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniq  10937  resqrexlemdecn  10954  resqrexlemcalc3  10958  resqrexlemcvg  10961  resqrexlemoverl  10963  leabs  11016  absexpzap  11022  ltabs  11029  abslt  11030  absle  11031  maxleim  11147  maxabslemval  11150  fimaxre2  11168  minmax  11171  2zinfmin  11184  xrmaxiflemcl  11186  xrmaxifle  11187  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxiflemcom  11190  xrmaxltsup  11199  xrmaxadd  11202  xrminmax  11206  xrbdtri  11217  2clim  11242  climshftlemg  11243  climsqz  11276  climsqz2  11277  climrecvg1n  11289  climcvg1nlem  11290  serf0  11293  sumrbdclem  11318  fsum3cvg  11319  summodclem3  11321  summodclem2a  11322  summodclem2  11323  zsumdc  11325  fsum3  11328  isumss  11332  fisumss  11333  fsum3cvg3  11337  fsumcl2lem  11339  fsumadd  11347  fsumsplit  11348  sumsnf  11350  fsum2d  11376  fisum0diag2  11388  fsummulc2  11389  modfsummod  11399  fsumabs  11406  fsumrelem  11412  fsumiun  11418  geoisumr  11459  cvgratnnlemseq  11467  cvgratz  11473  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodrbdclem  11512  fproddccvg  11513  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodntrivap  11525  fprodssdc  11531  fprodmul  11532  prodsnf  11533  fprodsplitdc  11537  fprodsplit  11538  fprodunsn  11545  fprodcl2lem  11546  fprodap0  11562  fprod2d  11564  fprodrec  11570  fprodap0f  11577  efcj  11614  efaddlem  11615  tanaddaplem  11679  nndivides  11737  dvdsext  11793  divalglemeunn  11858  divalglemex  11859  divalglemeuneg  11860  zsupcllemstep  11878  infssuzex  11882  suprzubdc  11885  nninfdcex  11886  zsupssdc  11887  dvdsbnd  11889  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlemzz  11935  bezoutlemaz  11936  bezoutlembz  11937  bezoutlemeu  11940  bezoutlemle  11941  bezoutlemsup  11942  dfgcd3  11943  dfgcd2  11947  bezoutr1  11966  nnmindc  11967  dvdslcm  12001  lcmgcdlem  12009  qredeq  12028  qredeu  12029  divgcdcoprm0  12033  divgcdcoprmex  12034  cncongr1  12035  isprm2lem  12048  prmind2  12052  exprmfct  12070  prmdvdsfz  12071  isprm5lem  12073  prmexpb  12083  rpexp1i  12086  sqrt2irr  12094  sqne2sq  12109  nonsq  12139  phiprmpw  12154  eulerthlemrprm  12161  eulerthlema  12162  hashgcdeq  12171  phisum  12172  modprmn0modprm0  12188  pclemub  12219  pclemdc  12220  pcmul  12233  pcqmul  12235  pcdvdstr  12258  pcprmpw2  12264  difsqpwdvds  12269  pcmpt  12273  oddprmdvds  12284  prmpwdvds  12285  pockthg  12287  infpnlem1  12289  1arith  12297  4sqlem2  12319  ennnfonelemg  12336  ennnfoneleminc  12344  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemfun  12350  ennnfonelemf1  12351  ennnfonelemrn  12352  ennnfonelemdm  12353  ennnfonelemnn0  12355  ennnfonelemim  12357  exmidunben  12359  ctinfomlemom  12360  ctinf  12363  ctiunctlemudc  12370  nninfdclemlt  12384  nninfdclemf1  12385  isstruct2r  12405  tgdom  12712  neipsm  12794  tgrest  12809  cnfval  12834  cnpfval  12835  cnpval  12838  iscnp4  12858  cnpnei  12859  cnptopco  12862  cncnpi  12868  cncnp  12870  cnptopresti  12878  cnptoprest2  12880  cndis  12881  lmtopcnp  12890  txbasval  12907  neitx  12908  txcnp  12911  txcnmpt  12913  txcn  12915  imasnopn  12939  psmetres2  12973  isxmet2d  12988  xblss2ps  13044  xblss2  13045  blbas  13073  neibl  13131  metss2lem  13137  metrest  13146  xmettx  13150  metcnp3  13151  metcnp  13152  metcnp2  13153  metcnpi  13155  metcnpi2  13156  mulc1cncf  13216  cncfco  13218  mulcncflem  13230  mulcncf  13231  dedekindeulemuub  13235  dedekindeulemloc  13237  dedekindeulemlu  13239  dedekindeu  13241  suplociccreex  13242  suplociccex  13243  dedekindicclemuub  13244  dedekindicclemloc  13246  dedekindicclemlu  13248  dedekindicclemicc  13250  dedekindicc  13251  ivthinclemlopn  13254  ivthinclemlr  13255  ivthinclemuopn  13256  ivthinclemur  13257  ivthinclemloc  13259  ivthinc  13261  limcimolemlt  13273  limccnp2lem  13285  limccnp2cntop  13286  limccoap  13287  dvcj  13313  dveflem  13327  efltlemlt  13335  sin0pilem1  13342  sin0pilem2  13343  pilem3  13344  coseq0negpitopi  13397  abssinper  13407  cos02pilt1  13412  relogeftb  13426  logbgcd1irraplemexp  13526  logbgcd1irrap  13528  lgsval  13545  lgsfvalg  13546  lgsfcl2  13547  lgsval2lem  13551  lgsmod  13567  lgsdilem  13568  lgsdir2lem4  13572  lgsdir2  13574  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  lgsdirnn0  13588  lgsdinn0  13589  2sqlem5  13595  2sqlem6  13596  2sqlem7  13597  2sqlem9  13600  2sqlem10  13601  bj-findis  13861  pwle2  13878  pwf1oexmid  13879  pw1nct  13883  nnsf  13885  peano4nninf  13886  nninfall  13889  nninfsellemeq  13894  nninfsellemeqinf  13896  qdencn  13906  refeq  13907  trilpolemeq1  13919  trilpolemlt1  13920  trirec0  13923  nconstwlpolemgt0  13942  nconstwlpolem  13943  neapmkvlem  13945