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  6415  enq0tr  6417  enq0eceq  6420  nqnq0pi  6421  nqnq0  6424  addcmpblnq0  6426  mulnnnq0  6433  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  distrnq0  6442  addassnq0  6445  nq02m  6448  preqlu  6455  prubl  6469  prloc  6474  prarloclemlt  6476  prarloclemn  6482  prarloc  6486  prarloc2  6487  genpml  6500  genpmu  6501  genpcdl  6502  genpcuu  6503  genprndl  6504  genprndu  6505  genpassl  6507  genpassu  6508  addlocprlemeq  6516  addlocprlemgt  6517  addlocpr  6519  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  addnqprlemfl  6540  addnqprlemfu  6541  appdivnq  6544  appdiv0nq  6545  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  mullocpr  6552  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  ltprordil  6565  1idprl  6566  1idpru  6567  ltpopr  6569  ltsopr  6570  ltaddpr  6571  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  addcanprleml  6588  addcanprlemu  6589  addcanprg  6590  ltaprlem  6591  addextpr  6593  recexprlemell  6594  recexprlemelu  6595  recexprlemm  6596  recexprlemdisj  6602  recexprlempr  6604  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  aptiprleml  6611  aptiprlemu  6612  ltmprr  6614  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlem2  6632  cauappcvgprlemlim  6633  archrecnq  6635  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemopu  6642  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlem2  6651  enreceq  6664  mulcmpblnrlemg  6668  ltsrprg  6675  recexgt0sr  6701  addgt0sr  6703  mulgt0sr  6704  archsr  6708  pitonn  6744  ax0id  6762  ltxrlt  6882  lttri3  6895  ltnsym  6901  ltletr  6904  muladd11  6943  readdcan  6950  cnegexlem1  6983  cnegexlem2  6984  cnegexlem3  6985  cnegex  6986  negeu  6999  npncan2  7034  subneg  7056  negcon1  7059  ltleadd  7236  lt2sub  7250  le2sub  7251  lenegcon1  7256  addge01  7262  leaddle0  7267  mullt0  7270  recexre  7362  reapti  7363  rimul  7369  apreap  7371  ltmul1  7376  apreim  7387  apcotr  7391  mulext1  7396  mulge0  7403  apti  7406  ltleap  7413  recextlem1  7414  recexaplem2  7415  recexap  7416  mulcanapd  7424  divmul13ap  7473  conjmulap  7487  p1le  7596  recgt0  7597  prodgt0gt0  7598  prodgt0  7599  lemul2a  7606  ltmul12a  7607  mulgt1  7610  lemulge12  7614  ltdivmul  7623  ltrec1  7635  ledivdiv  7637  lediv2a  7642  cju  7694  nn1suc  7714  nnmulcl  7716  nn2ge  7727  nnsub  7733  halfaddsub  7936  nnrecl  7955  nn0ge2m1nn  8018  nn0nndivcl  8020  elnn0z  8034  peano2z  8057  zaddcllempos  8058  zaddcllemneg  8060  zaddcl  8061  ztri3or  8064  zletric  8065  zlelttric  8066  zleloe  8068  zrevaddcl  8071  zltp1le  8074  zlem1lt  8076  elz2  8088  zdceq  8092  zdcle  8093  zdclt  8094  nn0n0n1ge2b  8096  nn0lt2  8098  nn0ge0div  8103  zdiv  8104  zdivadd  8105  zdivmul  8106  zextle  8107  msqznn  8114  zneo  8115  zeo  8119  peano5uzti  8122  nn0ind-raph  8131  uztrn  8265  uzss  8269  eluzadd  8277  uzaddcl  8305  indstr  8312  indstr2  8322  nn0ge2m1nnALT  8329  qmulz  8334  qaddcl  8346  qnegcl  8347  qmulcl  8348  qreccl  8351  qrevaddcl  8353  ge0p1rp  8389  rpnegap  8390  ltxr  8465  xrltnsym  8484  xrlttr  8486  xrltso  8487  xrlttri3  8488  xrltletr  8493  xrre2  8504  ge0nemnf  8507  xltnegi  8518  lbioog  8552  iccss2  8583  iccssioo2  8585  iccssico2  8586  iooshf  8591  elioopnf  8606  elioomnf  8607  elicopnf  8608  elxrge0  8617  icoshftf1o  8629  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  lincmb01cmp  8641  iccf1o  8642  elfz5  8652  fztri3or  8673  fznlem  8675  fzn  8676  uzsubsubfz  8681  fzdisj  8686  fzmmmeqm  8691  fzaddel  8692  fzopth  8694  fznatpl1  8708  fzdifsuc  8713  elfz1b  8722  fseq1p1m1  8726  elfzp1b  8729  fzm1  8732  fzneuz  8733  ige2m1fz  8742  elfz0addOLD  8750  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  difelfzle  8762  difelfznle  8763  nn0disj  8765  1fv  8766  4fvwrd4  8767  fzoss1  8797  fzospliti  8802  fzosplit  8803  fzouzdisj  8806  fzo1fzo0n0  8809  elfzo0z  8810  fzonmapblen  8813  fzofzim  8814  fzoaddel  8818  fzosubel  8820  fzosubel3  8822  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  elfzom1elp1fzo  8828  zpnn0elfzo1  8834  elfzom1p1elfzo  8840  ssfzo12  8850  ssfzo12bi  8851  ubmelm1fzo  8852  elfzonelfzo  8856  elfzomelpfzo  8857  fzoshftral  8864  frec2uzltd  8870  frec2uzlt2d  8871  frec2uzrand  8872  frec2uzf1od  8873  frec2uzisod  8874  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgfn  8879  frecuzrdgcl  8880  frecuzrdgsuc  8882  frecfzennn  8884  iseqovex  8899  iseqval  8900  iseqfveq2  8905  iseqfeq2  8906  expivallem  8910  expival  8911  expp1  8916  expn1ap0  8919  expcllem  8920  expcl2lemap  8921  rpexpcl  8928  m1expcl2  8931  expclzaplem  8933  1exp  8938  expap0  8939  expeq0  8940  expnegzap  8943  mulexp  8948  expadd  8951  expaddzaplem  8952  expmul  8954  leexp2r  8962  leexp1a  8963  expubnd  8965  sqgt0ap  8975  subsq  9011  binom2sub  9017  zesq  9020  bernneq  9022  bernneq3  9024  expnbnd  9025  expnlbnd  9026  crre  9085  reim0b  9090  rereb  9091  mulreap  9092  readd  9097  remullem  9099  remul2  9101  imadd  9105  immul2  9108  cjadd  9112  cjexp  9121  cjap  9134  absnid  9227  nn0abscl  9229  peano5setOLD  9400  sscoll2  9448
  Copyright terms: Public domain W3C validator