ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantr Unicode version

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
StepHypRef Expression
1 adantr.1 . . 3  |-  ( ph  ->  ps )
21a1d 22 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 115 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
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  ordiso2  6355  ordiso  6356  carden2bex  6367  elni2  6410  mulclpi  6424  addasspig  6426  mulasspig  6428  mulcanpig  6431  ltexpi  6433  ltapig  6434  ltmpig  6435  indpi  6438  enqeceq  6455  addcmpblnq  6463  dmaddpqlem  6473  distrnqg  6483  mulidnq  6485  ltsonq  6494  ltexnqq  6504  subhalfnqq  6510  ltbtwnnqq  6511  ltbtwnnq  6512  archnqq  6513  ltrnqg  6516  enq0sym  6528  enq0tr  6530  enq0eceq  6533  nqnq0pi  6534  nqnq0  6537  addcmpblnq0  6539  mulnnnq0  6546  nqpnq0nq  6549  nqnq0a  6550  nqnq0m  6551  nq0m0r  6552  distrnq0  6555  addassnq0  6558  nq02m  6561  preqlu  6568  prubl  6582  prloc  6587  prarloclemlt  6589  prarloclemn  6595  prarloc  6599  prarloc2  6600  genpml  6613  genpmu  6614  genpcdl  6615  genpcuu  6616  genprndl  6617  genprndu  6618  genpassl  6620  genpassu  6621  addlocprlemeq  6629  addlocprlemgt  6630  addlocpr  6632  nqprl  6647  nqpru  6648  addnqprlemrl  6653  addnqprlemru  6654  addnqprlemfl  6655  addnqprlemfu  6656  appdivnq  6659  appdiv0nq  6660  mulnqprl  6664  mulnqpru  6665  mullocprlem  6666  mullocpr  6667  mulnqprlemrl  6669  mulnqprlemru  6670  mulnqprlemfl  6671  mulnqprlemfu  6672  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  ltprordil  6685  1idprl  6686  1idpru  6687  ltpopr  6691  ltsopr  6692  ltaddpr  6693  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemloc  6703  ltexprlemrl  6706  ltexprlemru  6708  addcanprleml  6710  addcanprlemu  6711  addcanprg  6712  ltaprlem  6714  prplnqu  6716  addextpr  6717  recexprlemell  6718  recexprlemelu  6719  recexprlemm  6720  recexprlemdisj  6726  recexprlempr  6728  recexprlem1ssl  6729  recexprlem1ssu  6730  recexprlemss1l  6731  recexprlemss1u  6732  aptiprleml  6735  aptiprlemu  6736  ltmprr  6738  cauappcvgprlemopu  6744  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  cauappcvgprlem2  6756  cauappcvgprlemlim  6757  archrecnq  6759  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemopu  6767  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemladdfu  6773  caucvgprlem2  6776  caucvgprprlemval  6784  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnjltk  6787  caucvgprprlemnbj  6789  caucvgprprlemmu  6791  caucvgprprlemopl  6793  caucvgprprlemopu  6795  caucvgprprlemdisj  6798  caucvgprprlemloc  6799  caucvgprprlemexbt  6802  caucvgprprlemexb  6803  caucvgprprlemaddq  6804  caucvgprprlem2  6806  enreceq  6819  mulcmpblnrlemg  6823  ltsrprg  6830  recexgt0sr  6856  addgt0sr  6858  mulgt0sr  6860  archsr  6864  prsrriota  6870  caucvgsrlemcau  6875  caucvgsrlemgt1  6877  caucvgsrlemoffval  6878  caucvgsrlemofff  6879  caucvgsrlemoffcau  6880  caucvgsrlemoffgt1  6881  caucvgsrlemoffres  6882  caucvgsr  6884  pitonn  6922  ltrennb  6928  ax0id  6950  rereceu  6961  recriota  6962  axcaucvglemval  6969  axcaucvglemcau  6970  axcaucvglemres  6971  ltxrlt  7083  lttri3  7096  ltnsym  7102  ltletr  7105  muladd11  7144  readdcan  7151  cnegexlem1  7184  cnegexlem2  7185  cnegexlem3  7186  cnegex  7187  negeu  7200  npncan2  7236  subneg  7258  negcon1  7261  lelttrdi  7419  ltleadd  7439  lt2sub  7453  le2sub  7454  lenegcon1  7459  addge01  7465  leaddle0  7470  mullt0  7473  recexre  7567  reapti  7568  rimul  7574  apreap  7576  ltmul1  7581  apreim  7592  apcotr  7596  mulext1  7601  mulge0  7608  apti  7611  ltleap  7619  recextlem1  7630  recexaplem2  7631  recexap  7632  mulcanapd  7640  divmul13ap  7689  conjmulap  7703  p1le  7813  recgt0  7814  prodgt0gt0  7815  prodgt0  7816  lemul2a  7823  ltmul12a  7824  mulgt1  7827  lemulge12  7831  ltdivmul  7840  ltrec1  7852  ledivdiv  7854  lediv2a  7859  cju  7911  nn1suc  7931  nnmulcl  7933  nn2ge  7944  nnsub  7950  halfaddsub  8157  div4p1lem1div2  8175  nnrecl  8177  nn0ge2m1nn  8240  nn0nndivcl  8242  elnn0z  8256  peano2z  8279  zaddcllempos  8280  zaddcllemneg  8282  zaddcl  8283  ztri3or  8286  zletric  8287  zlelttric  8288  zleloe  8290  zrevaddcl  8293  zltp1le  8296  zlem1lt  8298  elz2  8310  zdceq  8314  zdcle  8315  zdclt  8316  nn0n0n1ge2b  8318  nn0lt2  8320  nn0ge0div  8325  zdiv  8326  zdivadd  8327  zdivmul  8328  zextle  8329  msqznn  8336  zneo  8337  zeo  8341  peano5uzti  8344  nn0ind-raph  8353  uztrn  8487  uzss  8491  eluzadd  8499  uzaddcl  8527  indstr  8534  indstr2  8544  nn0ge2m1nnALT  8551  qmulz  8556  qaddcl  8568  qnegcl  8569  qmulcl  8570  qreccl  8574  qrevaddcl  8576  ge0p1rp  8612  rpnegap  8613  divlt1lt  8648  divle1le  8649  ledivge1le  8650  ltxr  8693  xrltnsym  8712  xrlttr  8714  xrltso  8715  xrlttri3  8716  xrltletr  8721  xrre2  8732  ge0nemnf  8735  xltnegi  8746  lbioog  8780  iccss2  8811  iccssioo2  8813  iccssico2  8814  iooshf  8819  elioopnf  8834  elioomnf  8835  elicopnf  8836  elxrge0  8845  icoshftf1o  8857  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  lincmb01cmp  8869  iccf1o  8870  elfz5  8880  fztri3or  8901  fznlem  8903  fzn  8904  uzsubsubfz  8909  fzdisj  8914  fzmmmeqm  8919  fzaddel  8920  fzopth  8922  fznatpl1  8936  fzdifsuc  8941  elfz1b  8950  fseq1p1m1  8954  elfzp1b  8957  fzm1  8960  fzneuz  8961  ige2m1fz  8970  elfz0addOLD  8978  elfz0ubfz0  8980  elfz0fzfz0  8981  fz0fzelfz0  8982  fz0fzdiffz0  8985  elfzmlbmOLD  8987  elfzmlbp  8988  difelfzle  8990  difelfznle  8991  nn0disj  8993  1fv  8994  4fvwrd4  8995  fzoss1  9025  fzospliti  9030  fzosplit  9031  fzouzdisj  9034  fzo1fzo0n0  9037  elfzo0z  9038  fzonmapblen  9041  fzofzim  9042  fzoaddel  9046  fzosubel  9048  fzosubel3  9050  eluzgtdifelfzo  9051  elfzodifsumelfzo  9055  elfzom1elp1fzo  9056  zpnn0elfzo1  9062  elfzom1p1elfzo  9068  ssfzo12  9078  ssfzo12bi  9079  ubmelm1fzo  9080  elfzonelfzo  9084  elfzomelpfzo  9085  fzoshftral  9092  fvinim0ffz  9094  subfzo0  9095  qletric  9097  qlelttric  9098  qdceq  9100  qbtwnre  9109  flqge  9122  flqltnz  9127  flqbi  9130  flqge0nn0  9133  flqge1nn  9134  flqaddz  9137  btwnzge0  9140  flltdivnn0lt  9144  fldiv4p1lem1div2  9145  flqeqceilz  9158  frec2uzltd  9163  frec2uzlt2d  9164  frec2uzrand  9165  frec2uzf1od  9166  frec2uzisod  9167  frecuzrdgrrn  9168  frec2uzrdg  9169  frecuzrdgfn  9172  frecuzrdgcl  9173  frecuzrdgsuc  9175  frecfzennn  9177  iseqovex  9193  iseqval  9194  iseqf  9198  iseqss  9200  iseqfveq2  9202  iseqfeq2  9203  iseqfeq  9205  iseqshft2  9206  monoord  9209  monoord2  9210  isermono  9211  iseqsplit  9212  iseqcaopr3  9214  iseqcaopr2  9215  iseqid3  9219  iseqid3s  9220  iseqid  9221  iseqhomo  9222  iseqdistr  9223  expivallem  9230  expival  9231  expp1  9236  expn1ap0  9239  expcllem  9240  expcl2lemap  9241  rpexpcl  9248  m1expcl2  9251  expclzaplem  9253  1exp  9258  expap0  9259  expeq0  9260  expnegzap  9263  mulexp  9268  expadd  9271  expaddzaplem  9272  expmul  9274  leexp2r  9282  leexp1a  9283  expubnd  9285  sqgt0ap  9296  subsq  9332  binom2sub  9338  zesq  9341  bernneq  9343  bernneq3  9345  expnbnd  9346  expnlbnd  9347  shftlem  9391  shftuz  9392  shftfvalg  9393  shftfval  9396  shftfn  9399  shftval3  9402  shftcan2  9410  crre  9431  reim0b  9436  rereb  9437  mulreap  9438  readd  9443  remullem  9445  remul2  9447  imadd  9451  immul2  9454  cjadd  9458  cjexp  9467  cjap  9480  caucvgre  9554  cvg1nlemf  9556  cvg1nlemres  9558  cvg1n  9559  rexanuz2  9563  recvguniq  9567  resqrexlem1arp  9577  resqrexlemp1rp  9578  resqrexlemfp1  9581  resqrexlemover  9582  resqrexlemdec  9583  resqrexlemlo  9585  resqrexlemcalc1  9586  resqrexlemcalc2  9587  resqrexlemcalc3  9588  resqrexlemnm  9590  resqrexlemcvg  9591  resqrexlemgt0  9592  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemga  9595  resqrexlemex  9597  rersqrtthlem  9602  sqrtmul  9607  sqrtsq2  9615  absrpclap  9633  absnid  9645  absexp  9649  absexpzap  9650  nn0abscl  9655  ltabs  9657  lenegsq  9665  recvalap  9667  nnabscl  9670  fzomaxdiflem  9682  fzomaxdif  9683  cau3lem  9684  clim  9776  climconst  9785  climconst2  9786  climuni  9788  climmpt  9795  2clim  9796  climshft2  9801  climcn1  9803  climcn2  9804  mulcn2  9807  climge0  9819  climadd  9820  climmul  9821  climsub  9822  climaddc1  9823  climaddc2  9824  climmulc2  9825  climsubc1  9826  climsubc2  9827  climsqz  9829  climsqz2  9830  clim2iser  9831  clim2iser2  9832  iiserex  9833  iisermulc2  9834  climlec2  9835  iserile  9836  climrecvg1n  9841  nn0seqcvgd  9854  ialgrlem1st  9855  ialgrlemconst  9856  ialgrp1  9859  algcvgblem  9862  ialgcvga  9864  peano5setOLD  10039  sscoll2  10087
  Copyright terms: Public domain W3C validator