Theorem adantr 261

Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
adantr.1	|- ( ph -> ps )

Assertion

Ref	Expression
adantr	|- ( ( ph /\ ch ) -> ps )

Proof of Theorem adantr

Step	Hyp	Ref	Expression
1		adantr.1	. . 3 |- ( ph -> ps )
2	1	a1d 22	. 2 |- ( ph -> ( ch -> ps ) )
3	2	imp 115	1 |- ( ( ph /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem is referenced by:  adantl  262  anim12ii  325  sylan9bb  435  ad2antrr  457  ad2antlr  458  ad2antrl  459  ad3antrrr  461  ad3antlr  462  ad4antr  463  ad4antlr  464  ad5antr  465  ad5antlr  466  ad6antr  467  ad6antlr  468  ad7antr  469  ad7antlr  470  ad8antr  471  ad8antlr  472  ad9antr  473  ad9antlr  474  ad10antr  475  ad10antlr  476  im2anan9  530  bi2bian9  540  jaao  639  ordi  729  con1bidc  768  con1bdc  772  pm5.18dc  777  dfandc  778  pm4.54dc  805  stabtestimpdc  824  ccase2  873  simpl1  907  simpl2  908  simpl3  909  3ad2ant1  925  3ad2ant2  926  simpll1  943  simpll2  944  simpll3  945  simplr1  946  simplr2  947  simplr3  948  simpl1l  955  simpl1r  956  simpl2l  957  simpl2r  958  simpl3l  959  simpl3r  960  simpl11  979  simpl12  980  simpl13  981  simpl21  982  simpl22  983  simpl23  984  simpl31  985  simpl32  986  simpl33  987  xorbin  1275  biassdc  1286  bilukdc  1287  sbequi  1720  nfsbxyt  1819  euan  1956  datisi  2010  fresison  2018  ralbid  2324  rexbid  2325  ralimdv  2388  reubidv  2493  rmobidv  2498  rabbidv  2549  elex22  2569  gencbvex  2600  rspct  2649  ceqsrexbv  2675  elrabf  2696  eueq3dc  2715  reu6  2730  reuind  2744  csbcomg  2873  csbiebt  2886  eldif  2927  sseq1  2966  undif3ss  3198  difrab  3211  ifcldcd  3358  disjpr2  3434  diftpsn3  3505  preqr1g  3537  nfopd  3566  eluni  3583  dfnfc2  3598  iuneq12d  3681  iuneq2d  3682  disjeq12d  3754  disjxsn  3762  mpteq12dv  3839  mpteq2dv  3848  trel  3861  csbexga  3885  opexg  3964  opexgOLD  3965  opm  3971  copsexg  3981  euotd  3991  elopab  3995  epelg  4027  sotritrieq  4062  frirrg  4087  wepo  4096  alxfr  4193  rexxfrd  4195  op1stbg  4210  ordelsuc  4231  onsucelsucr  4234  onintonm  4243  onsucelsucexmidlem  4254  reg2exmidlema  4259  en2lp  4278  preleq  4279  opthreg  4280  ordsuc  4287  onsucuni2  4288  onintexmid  4297  wetriext  4301  reg3exmidlemwe  4303  peano5  4321  poinxp  4409  sosng  4413  eqrelrdv2  4439  xpsspw  4450  relopabi  4463  opeliunxp2  4476  relop  4486  opeldmg  4540  xpid11m  4557  riinint  4593  asymref  4710  xpidtr  4715  ssxpbm  4756  ssxp1  4757  ssxp2  4758  xpexr2m  4762  rnpropg  4800  elxp4  4808  elxp5  4809  funeu  4926  funun  4944  fununi  4967  funimaexglem  4982  funfni  4999  fneu  5003  fco  5056  funssxp  5060  feu  5072  fimacnvdisj  5074  f1ss  5097  f1ssr  5098  f1ssres  5099  f1imacnv  5143  foimacnv  5144  fun11iun  5147  f1o00  5161  nffvd  5187  fnbrfvb  5214  fvelrnb  5221  fvelimab  5229  ssimaex  5234  fvopab3g  5245  fvmptssdm  5255  fvmpt2d  5257  fvmptdf  5258  eqfnfv  5265  fndmdif  5272  fndmin  5274  fneqeql2  5276  fvimacnv  5282  ffvelrn  5300  dff3im  5312  dffo3  5314  fmptco  5330  fcompt  5333  fsn2  5337  fprg  5346  fvunsng  5357  fsnunres  5364  resfunexg  5382  fnex  5383  f1ocnvfv1  5417  f1ocnvfv2  5418  foeqcnvco  5430  f1eqcocnv  5431  fliftf  5439  fliftval  5440  isocnv  5451  isocnv2  5452  isores3  5455  isoini  5457  isoini2  5458  isoselem  5459  riotaexg  5472  riota2df  5488  acexmid  5511  oprabid  5537  0neqopab  5550  mpt2eq123dv  5567  cbvmpt2x  5582  eloprabga  5591  ovmpt2dxf  5626  ovmpt2df  5632  ov6g  5638  oprssov  5642  caovord3  5674  caovimo  5694  grprinvlem  5695  grprinvd  5696  f1opw2  5706  suppssfv  5708  suppssov1  5709  fnofval  5721  off  5724  offval2  5726  ofrfval2  5727  ofc12  5731  caofref  5732  caofinvl  5733  caofrss  5735  caoftrn  5736  fnexALT  5740  iunexg  5746  offval3  5761  f1stres  5786  elxp6  5796  elxp7  5797  unielxp  5800  xpopth  5802  op1steq  5805  releldm2  5811  dfoprab4  5818  fmpt2x  5826  1stconst  5842  2ndconst  5843  cnvf1o  5846  f1o2ndf1  5849  mpt2xopoveq  5855  isprmpt2  5858  brtpos2  5866  smores2  5909  iordsmo  5912  smoiso  5917  tfrlem1  5923  tfrlem3a  5925  tfrlem4  5929  tfrlem8  5934  tfrlemisucaccv  5939  tfrlemiubacc  5944  tfrlemi1  5946  tfri3  5953  rdgivallem  5968  rdgon  5973  frecrdg  5992  freccl  5993  sucinc2  6026  oav2  6043  oaword1  6050  nnmcl  6060  nndi  6065  nntri2or2  6076  nnaordi  6081  nnaword  6084  nnmordi  6089  nnmord  6090  nnaordex  6100  nnawordex  6101  nnm00  6102  ersymb  6120  erref  6126  iserd  6132  erth  6150  erinxp  6180  qliftel  6186  qliftfun  6188  eroveu  6197  eroprf  6199  th3qlem1  6208  ecovass  6215  ecoviass  6216  dom2lem  6252  ssdomg  6258  fundmen  6286  cnven  6288  fndmeng  6289  xpsnen  6295  xpdom2  6305  fopwdom  6310  phplem2  6316  nneneq  6320  nndomo  6326  phpm  6327  fidifsnen  6331  dif1en  6337  php5fin  6339  fin0  6342  fin0or  6343  findcard2  6346  findcard2s  6347  findcard2d  6348  findcard2sd  6349  diffisn  6350  diffifi  6351  fientri3  6353  onunsnss  6355  snon0  6356  ordiso2  6357  ordiso  6358  carden2bex  6369  elni2  6412  mulclpi  6426  addasspig  6428  mulasspig  6430  mulcanpig  6433  ltexpi  6435  ltapig  6436  ltmpig  6437  indpi  6440  enqeceq  6457  addcmpblnq  6465  dmaddpqlem  6475  distrnqg  6485  mulidnq  6487  ltsonq  6496  ltexnqq  6506  subhalfnqq  6512  ltbtwnnqq  6513  ltbtwnnq  6514  archnqq  6515  ltrnqg  6518  enq0sym  6530  enq0tr  6532  enq0eceq  6535  nqnq0pi  6536  nqnq0  6539  addcmpblnq0  6541  mulnnnq0  6548  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  distrnq0  6557  addassnq0  6560  nq02m  6563  preqlu  6570  prubl  6584  prloc  6589  prarloclemlt  6591  prarloclemn  6597  prarloc  6601  prarloc2  6602  genpml  6615  genpmu  6616  genpcdl  6617  genpcuu  6618  genprndl  6619  genprndu  6620  genpassl  6622  genpassu  6623  addlocprlemeq  6631  addlocprlemgt  6632  addlocpr  6634  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  addnqprlemfl  6657  addnqprlemfu  6658  appdivnq  6661  appdiv0nq  6662  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  mullocpr  6669  mulnqprlemrl  6671  mulnqprlemru  6672  mulnqprlemfl  6673  mulnqprlemfu  6674  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  ltprordil  6687  1idprl  6688  1idpru  6689  ltpopr  6693  ltsopr  6694  ltaddpr  6695  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  addcanprleml  6712  addcanprlemu  6713  addcanprg  6714  ltaprlem  6716  prplnqu  6718  addextpr  6719  recexprlemell  6720  recexprlemelu  6721  recexprlemm  6722  recexprlemdisj  6728  recexprlempr  6730  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  recexprlemss1u  6734  aptiprleml  6737  aptiprlemu  6738  ltmprr  6740  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgprlemlim  6759  archrecnq  6761  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemopu  6769  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlem2  6778  caucvgprprlemval  6786  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemnbj  6791  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemdisj  6800  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlem2  6808  enreceq  6821  mulcmpblnrlemg  6825  ltsrprg  6832  recexgt0sr  6858  addgt0sr  6860  mulgt0sr  6862  archsr  6866  prsrriota  6872  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsrlemofff  6881  caucvgsrlemoffcau  6882  caucvgsrlemoffgt1  6883  caucvgsrlemoffres  6884  caucvgsr  6886  pitonn  6924  ltrennb  6930  ax0id  6952  rereceu  6963  recriota  6964  axcaucvglemval  6971  axcaucvglemcau  6972  axcaucvglemres  6973  ltxrlt  7085  lttri3  7098  ltnsym  7104  ltletr  7107  muladd11  7146  readdcan  7153  cnegexlem1  7186  cnegexlem2  7187  cnegexlem3  7188  cnegex  7189  negeu  7202  npncan2  7238  subneg  7260  negcon1  7263  lelttrdi  7421  ltleadd  7441  lt2sub  7455  le2sub  7456  lenegcon1  7461  addge01  7467  leaddle0  7472  mullt0  7475  recexre  7569  reapti  7570  rimul  7576  apreap  7578  ltmul1  7583  apreim  7594  apcotr  7598  mulext1  7603  mulge0  7610  apti  7613  ltleap  7621  recextlem1  7632  recexaplem2  7633  recexap  7634  mulcanapd  7642  divmul13ap  7691  conjmulap  7705  p1le  7815  recgt0  7816  prodgt0gt0  7817  prodgt0  7818  lemul2a  7825  ltmul12a  7826  mulgt1  7829  lemulge12  7833  ltdivmul  7842  ltrec1  7854  ledivdiv  7856  lediv2a  7861  cju  7913  nn1suc  7933  nnmulcl  7935  nn2ge  7946  nnsub  7952  halfaddsub  8159  div4p1lem1div2  8177  nnrecl  8179  nn0ge2m1nn  8242  nn0nndivcl  8244  elnn0z  8258  peano2z  8281  zaddcllempos  8282  zaddcllemneg  8284  zaddcl  8285  ztri3or  8288  zletric  8289  zlelttric  8290  zleloe  8292  zrevaddcl  8295  zltp1le  8298  zlem1lt  8300  elz2  8312  zdceq  8316  zdcle  8317  zdclt  8318  nn0n0n1ge2b  8320  nn0lt2  8322  nn0ge0div  8327  zdiv  8328  zdivadd  8329  zdivmul  8330  zextle  8331  msqznn  8338  zneo  8339  zeo  8343  peano5uzti  8346  nn0ind-raph  8355  uztrn  8489  uzss  8493  eluzadd  8501  uzaddcl  8529  indstr  8536  indstr2  8546  nn0ge2m1nnALT  8553  qmulz  8558  qaddcl  8570  qnegcl  8571  qmulcl  8572  qreccl  8576  qrevaddcl  8578  ge0p1rp  8614  rpnegap  8615  divlt1lt  8650  divle1le  8651  ledivge1le  8652  ltxr  8695  xrltnsym  8714  xrlttr  8716  xrltso  8717  xrlttri3  8718  xrltletr  8723  xrre2  8734  ge0nemnf  8737  xltnegi  8748  lbioog  8782  iccss2  8813  iccssioo2  8815  iccssico2  8816  iooshf  8821  elioopnf  8836  elioomnf  8837  elicopnf  8838  elxrge0  8847  icoshftf1o  8859  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  lincmb01cmp  8871  iccf1o  8872  elfz5  8882  fztri3or  8903  fznlem  8905  fzn  8906  uzsubsubfz  8911  fzdisj  8916  fzmmmeqm  8921  fzaddel  8922  fzopth  8924  fznatpl1  8938  fzdifsuc  8943  elfz1b  8952  fseq1p1m1  8956  elfzp1b  8959  fzm1  8962  fzneuz  8963  ige2m1fz  8972  elfz0addOLD  8980  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  difelfzle  8992  difelfznle  8993  nn0disj  8995  1fv  8996  4fvwrd4  8997  fzoss1  9027  fzospliti  9032  fzosplit  9033  fzouzdisj  9036  fzo1fzo0n0  9039  elfzo0z  9040  fzonmapblen  9043  fzofzim  9044  fzoaddel  9048  fzosubel  9050  fzosubel3  9052  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  elfzom1elp1fzo  9058  zpnn0elfzo1  9064  elfzom1p1elfzo  9070  ssfzo12  9080  ssfzo12bi  9081  ubmelm1fzo  9082  elfzonelfzo  9086  elfzomelpfzo  9087  fzoshftral  9094  fvinim0ffz  9096  subfzo0  9097  qletric  9099  qlelttric  9100  qdceq  9102  qbtwnre  9111  flqge  9124  flqltnz  9129  flqbi  9132  flqge0nn0  9135  flqge1nn  9136  flqaddz  9139  btwnzge0  9142  flltdivnn0lt  9146  fldiv4p1lem1div2  9147  flqeqceilz  9160  intfracq  9162  flqdiv  9163  zmod1congr  9183  frec2uzltd  9189  frec2uzlt2d  9190  frec2uzrand  9191  frec2uzf1od  9192  frec2uzisod  9193  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgfn  9198  frecuzrdgcl  9199  frecuzrdgsuc  9201  frecfzennn  9203  iseqovex  9219  iseqval  9220  iseqf  9224  iseqss  9226  iseqfveq2  9228  iseqfeq2  9229  iseqfeq  9231  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqid3  9245  iseqid3s  9246  iseqid  9247  iseqhomo  9248  iseqdistr  9249  expivallem  9256  expival  9257  expp1  9262  expn1ap0  9265  expcllem  9266  expcl2lemap  9267  rpexpcl  9274  m1expcl2  9277  expclzaplem  9279  1exp  9284  expap0  9285  expeq0  9286  expnegzap  9289  mulexp  9294  expadd  9297  expaddzaplem  9298  expmul  9300  leexp2r  9308  leexp1a  9309  expubnd  9311  sqgt0ap  9322  subsq  9358  binom2sub  9364  zesq  9367  bernneq  9369  bernneq3  9371  expnbnd  9372  expnlbnd  9373  shftlem  9417  shftuz  9418  shftfvalg  9419  shftfval  9422  shftfn  9425  shftval3  9428  shftcan2  9436  crre  9457  reim0b  9462  rereb  9463  mulreap  9464  readd  9469  remullem  9471  remul2  9473  imadd  9477  immul2  9480  cjadd  9484  cjexp  9493  cjap  9506  caucvgre  9580  cvg1nlemf  9582  cvg1nlemres  9584  cvg1n  9585  rexanuz2  9589  recvguniq  9593  resqrexlem1arp  9603  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  resqrexlemex  9623  rersqrtthlem  9628  sqrtmul  9633  sqrtsq2  9641  absrpclap  9659  absnid  9671  absexp  9675  absexpzap  9676  nn0abscl  9681  ltabs  9683  lenegsq  9691  recvalap  9693  nnabscl  9696  fzomaxdiflem  9708  fzomaxdif  9709  cau3lem  9710  clim  9802  climconst  9811  climconst2  9812  climuni  9814  climmpt  9821  2clim  9822  climshft2  9827  climcn1  9829  climcn2  9830  mulcn2  9833  climge0  9845  climadd  9846  climmul  9847  climsub  9848  climaddc1  9849  climaddc2  9850  climmulc2  9851  climsubc1  9852  climsubc2  9853  climsqz  9855  climsqz2  9856  clim2iser  9857  clim2iser2  9858  iiserex  9859  iisermulc2  9860  climlec2  9861  iserile  9862  climrecvg1n  9867  nn0seqcvgd  9880  ialgrlem1st  9881  ialgrlemconst  9882  ialgrp1  9885  algcvgblem  9888  ialgcvga  9890  peano5setOLD  10065  sscoll2  10113  qdencn  10124