ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantr Structured version   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
Assertion
Ref Expression
adantr

Proof of Theorem adantr
StepHypRef Expression
1 adantr.1 . . 3
21a1d 22 . 2
32imp 115 1
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  638  ordi  728  con1bidc  767  con1bdc  771  pm5.18dc  776  dfandc  777  pm4.54dc  804  stabtestimpdc  823  ccase2  872  simpl1  906  simpl2  907  simpl3  908  3ad2ant1  924  3ad2ant2  925  simpll1  942  simpll2  943  simpll3  944  simplr1  945  simplr2  946  simplr3  947  simpl1l  954  simpl1r  955  simpl2l  956  simpl2r  957  simpl3l  958  simpl3r  959  simpl11  978  simpl12  979  simpl13  980  simpl21  981  simpl22  982  simpl23  983  simpl31  984  simpl32  985  simpl33  986  xorbin  1272  biassdc  1283  bilukdc  1284  sbequi  1717  nfsbxyt  1816  euan  1953  datisi  2007  fresison  2015  ralbid  2318  rexbid  2319  ralimdv  2382  reubidv  2487  rmobidv  2492  rabbidv  2543  elex22  2563  gencbvex  2594  rspct  2643  ceqsrexbv  2669  elrabf  2690  eueq3dc  2709  reu6  2724  reuind  2738  csbcomg  2867  csbiebt  2880  eldif  2921  sseq1  2960  undif3ss  3192  difrab  3205  disjpr2  3425  diftpsn3  3496  preqr1g  3528  nfopd  3557  eluni  3574  dfnfc2  3589  iuneq12d  3672  iuneq2d  3673  disjeq12d  3745  disjxsn  3753  mpteq12dv  3830  mpteq2dv  3839  trel  3852  csbexga  3876  opexg  3955  opexgOLD  3956  opm  3962  copsexg  3972  euotd  3982  elopab  3986  epelg  4018  sotritrieq  4053  alxfr  4159  rexxfrd  4161  op1stbg  4176  ordelsuc  4197  onsucelsucr  4199  onsucelsucexmidlem  4214  en2lp  4232  preleq  4233  opthreg  4234  ordsuc  4241  peano5  4264  poinxp  4352  sosng  4356  eqrelrdv2  4382  xpsspw  4393  relopabi  4406  opeliunxp2  4419  relop  4429  opeldmg  4483  xpid11m  4500  riinint  4536  asymref  4653  xpidtr  4658  ssxpbm  4699  ssxp1  4700  ssxp2  4701  xpexr2m  4705  rnpropg  4743  elxp4  4751  elxp5  4752  funeu  4869  funun  4887  fununi  4910  funimaexglem  4925  funfni  4942  fneu  4946  fco  4999  funssxp  5003  feu  5015  fimacnvdisj  5017  f1ss  5040  f1ssr  5041  f1ssres  5042  f1imacnv  5086  foimacnv  5087  fun11iun  5090  f1o00  5104  nffvd  5130  fnbrfvb  5157  fvelrnb  5164  fvelimab  5172  ssimaex  5177  fvopab3g  5188  fvmptssdm  5198  fvmpt2d  5200  fvmptdf  5201  eqfnfv  5208  fndmdif  5215  fndmin  5217  fneqeql2  5219  fvimacnv  5225  ffvelrn  5243  dff3im  5255  dffo3  5257  fmptco  5273  fcompt  5276  fsn2  5280  fprg  5289  fvunsng  5300  fsnunres  5307  resfunexg  5325  fnex  5326  f1ocnvfv1  5360  f1ocnvfv2  5361  foeqcnvco  5373  f1eqcocnv  5374  fliftf  5382  fliftval  5383  isocnv  5394  isocnv2  5395  isores3  5398  isoini  5400  isoini2  5401  isoselem  5402  riotaexg  5415  riota2df  5431  acexmid  5454  oprabid  5480  0neqopab  5492  mpt2eq123dv  5509  cbvmpt2x  5524  eloprabga  5533  ovmpt2dxf  5568  ovmpt2df  5574  ov6g  5580  oprssov  5584  caovord3  5616  caovimo  5636  grprinvlem  5637  grprinvd  5638  f1opw2  5648  suppssfv  5650  suppssov1  5651  fnofval  5663  off  5666  offval2  5668  ofrfval2  5669  ofc12  5673  caofref  5674  caofinvl  5675  caofrss  5677  caoftrn  5678  fnexALT  5682  iunexg  5688  offval3  5703  f1stres  5728  elxp6  5738  elxp7  5739  unielxp  5742  xpopth  5744  op1steq  5747  releldm2  5753  dfoprab4  5760  fmpt2x  5768  1stconst  5784  2ndconst  5785  cnvf1o  5788  f1o2ndf1  5791  mpt2xopoveq  5796  isprmpt2  5799  brtpos2  5807  smores2  5850  iordsmo  5853  smoiso  5858  tfrlem1  5864  tfrlem3a  5866  tfrlem4  5870  tfrlem8  5875  tfrlemisucaccv  5880  tfrlemiubacc  5885  tfrlemi1  5887  tfri3  5894  rdgivallem  5908  rdgon  5913  frecrdg  5931  freccl  5932  sucinc2  5965  oav2  5982  oaword1  5989  nnmcl  5999  nndi  6004  nnaordi  6017  nnaword  6020  nnmordi  6025  nnmord  6026  nnaordex  6036  nnawordex  6037  nnm00  6038  ersymb  6056  erref  6062  iserd  6068  erth  6086  erinxp  6116  qliftel  6122  qliftfun  6124  eroveu  6133  eroprf  6135  th3qlem1  6144  ecovass  6151  ecoviass  6152  dom2lem  6188  ssdomg  6194  fundmen  6222  cnven  6224  fndmeng  6225  xpsnen  6231  xpdom2  6241  fopwdom  6246  elni2  6298  mulclpi  6312  addasspig  6314  mulasspig  6316  mulcanpig  6319  ltexpi  6321  ltapig  6322  ltmpig  6323  indpi  6326  enqeceq  6343  addcmpblnq  6351  dmaddpqlem  6361  distrnqg  6371  mulidnq  6373  ltsonq  6382  ltexnqq  6391  subhalfnqq  6397  ltbtwnnqq  6398  ltbtwnnq  6399  archnqq  6400  ltrnqg  6403  enq0sym  6414  enq0tr  6416  enq0eceq  6419  nqnq0pi  6420  nqnq0  6423  addcmpblnq0  6425  mulnnnq0  6432  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  nq0m0r  6438  distrnq0  6441  addassnq0  6444  nq02m  6447  preqlu  6454  prubl  6468  prloc  6473  prarloclemlt  6475  prarloclemn  6481  prarloc  6485  prarloc2  6486  genpml  6499  genpmu  6500  genpcdl  6501  genpcuu  6502  genprndl  6503  genprndu  6504  genpassl  6506  genpassu  6507  addlocprlemeq  6515  addlocprlemgt  6516  addlocpr  6518  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  addnqprlemfl  6539  addnqprlemfu  6540  appdivnq  6543  appdiv0nq  6544  mulnqprl  6548  mulnqpru  6549  mullocprlem  6550  mullocpr  6551  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  ltprordil  6564  1idprl  6565  1idpru  6566  ltpopr  6568  ltsopr  6569  ltaddpr  6570  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  addcanprleml  6587  addcanprlemu  6588  addcanprg  6589  ltaprlem  6590  addextpr  6592  recexprlemell  6593  recexprlemelu  6594  recexprlemm  6595  recexprlemdisj  6601  recexprlempr  6603  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607  aptiprleml  6610  aptiprlemu  6611  ltmprr  6613  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlem2  6631  cauappcvgprlemlim  6632  enreceq  6644  mulcmpblnrlemg  6648  ltsrprg  6655  recexgt0sr  6681  addgt0sr  6683  mulgt0sr  6684  archsr  6688  pitonn  6724  ax0id  6742  ltxrlt  6862  lttri3  6875  ltnsym  6881  ltletr  6884  muladd11  6923  readdcan  6930  cnegexlem1  6963  cnegexlem2  6964  cnegexlem3  6965  cnegex  6966  negeu  6979  npncan2  7014  subneg  7036  negcon1  7039  ltleadd  7216  lt2sub  7230  le2sub  7231  lenegcon1  7236  addge01  7242  leaddle0  7247  mullt0  7250  recexre  7342  reapti  7343  rimul  7349  apreap  7351  ltmul1  7356  apreim  7367  apcotr  7371  mulext1  7376  mulge0  7383  apti  7386  ltleap  7393  recextlem1  7394  recexaplem2  7395  recexap  7396  mulcanapd  7404  divmul13ap  7453  conjmulap  7467  p1le  7576  recgt0  7577  prodgt0gt0  7578  prodgt0  7579  lemul2a  7586  ltmul12a  7587  mulgt1  7590  lemulge12  7594  ltdivmul  7603  ltrec1  7615  ledivdiv  7617  lediv2a  7622  cju  7674  nn1suc  7694  nnmulcl  7696  nn2ge  7707  nnsub  7713  halfaddsub  7916  nnrecl  7935  nn0ge2m1nn  7998  nn0nndivcl  8000  elnn0z  8014  peano2z  8037  zaddcllempos  8038  zaddcllemneg  8040  zaddcl  8041  ztri3or  8044  zletric  8045  zlelttric  8046  zleloe  8048  zrevaddcl  8051  zltp1le  8054  zlem1lt  8056  elz2  8068  zdceq  8072  zdcle  8073  zdclt  8074  nn0n0n1ge2b  8076  nn0lt2  8078  nn0ge0div  8083  zdiv  8084  zdivadd  8085  zdivmul  8086  zextle  8087  msqznn  8094  zneo  8095  zeo  8099  peano5uzti  8102  nn0ind-raph  8111  uztrn  8245  uzss  8249  eluzadd  8257  uzaddcl  8285  indstr  8292  indstr2  8302  nn0ge2m1nnALT  8309  qmulz  8314  qaddcl  8326  qnegcl  8327  qmulcl  8328  qreccl  8331  qrevaddcl  8333  ge0p1rp  8369  rpnegap  8370  ltxr  8445  xrltnsym  8464  xrlttr  8466  xrltso  8467  xrlttri3  8468  xrltletr  8473  xrre2  8484  ge0nemnf  8487  xltnegi  8498  lbioog  8532  iccss2  8563  iccssioo2  8565  iccssico2  8566  iooshf  8571  elioopnf  8586  elioomnf  8587  elicopnf  8588  elxrge0  8597  icoshftf1o  8609  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  lincmb01cmp  8621  iccf1o  8622  elfz5  8632  fztri3or  8653  fznlem  8655  fzn  8656  uzsubsubfz  8661  fzdisj  8666  fzmmmeqm  8671  fzaddel  8672  fzopth  8674  fznatpl1  8688  fzdifsuc  8693  elfz1b  8702  fseq1p1m1  8706  elfzp1b  8709  fzm1  8712  fzneuz  8713  ige2m1fz  8722  elfz0addOLD  8730  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzmlbmOLD  8739  elfzmlbp  8740  difelfzle  8742  difelfznle  8743  nn0disj  8745  1fv  8746  4fvwrd4  8747  fzoss1  8777  fzospliti  8782  fzosplit  8783  fzouzdisj  8786  fzo1fzo0n0  8789  elfzo0z  8790  fzonmapblen  8793  fzofzim  8794  fzoaddel  8798  fzosubel  8800  fzosubel3  8802  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  elfzom1elp1fzo  8808  zpnn0elfzo1  8814  elfzom1p1elfzo  8820  ssfzo12  8830  ssfzo12bi  8831  ubmelm1fzo  8832  elfzonelfzo  8836  elfzomelpfzo  8837  fzoshftral  8844  frec2uzltd  8850  frec2uzlt2d  8851  frec2uzrand  8852  frec2uzf1od  8853  frec2uzisod  8854  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgfn  8859  frecuzrdgcl  8860  frecuzrdgsuc  8862  frecfzennn  8864  iseqovex  8879  iseqval  8880  iseqfveq2  8885  iseqfeq2  8886  expivallem  8890  expival  8891  expp1  8896  expn1ap0  8899  expcllem  8900  expcl2lemap  8901  rpexpcl  8908  m1expcl2  8911  expclzaplem  8913  1exp  8918  expap0  8919  expeq0  8920  expnegzap  8923  mulexp  8928  expadd  8931  expaddzaplem  8932  expmul  8934  leexp2r  8942  leexp1a  8943  expubnd  8945  sqgt0ap  8955  subsq  8991  binom2sub  8997  zesq  9000  bernneq  9002  bernneq3  9004  expnbnd  9005  expnlbnd  9006  crre  9065  reim0b  9070  rereb  9071  mulreap  9072  readd  9077  remullem  9079  remul2  9081  imadd  9085  immul2  9088  cjadd  9092  cjexp  9101  cjap  9114  absnid  9207  nn0abscl  9209  peano5set  9374  sscoll2  9418
  Copyright terms: Public domain W3C validator