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

Theorem adantl 262
Description: Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
adantl.1
Assertion
Ref Expression
adantl

Proof of Theorem adantl
StepHypRef Expression
1 adantl.1 . . 3
21adantr 261 . 2
32ancoms 255 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  ax-ia3 101
This theorem is referenced by:  sylan2  270  anim12ii  325  sylan9bb  435  ad2antrl  459  ad2antll  460  im2anan9  530  bi2bian9  540  jaao  638  ordi  728  con1bidc  767  con1bdc  771  dfandc  777  stabtestimpdc  823  dcor  842  annimdc  844  ccase2  872  rnlem  882  simpr1  909  simpr2  910  simpr3  911  3ad2ant3  926  simprl1  948  simprl2  949  simprl3  950  simprr1  951  simprr2  952  simprr3  953  simpr1l  960  simpr1r  961  simpr2l  962  simpr2r  963  simpr3l  964  simpr3r  965  simpr11  987  simpr12  988  simpr13  989  simpr21  990  simpr22  991  simpr23  992  simpr31  993  simpr32  994  simpr33  995  falimd  1257  xorbin  1272  xor2dc  1278  biassdc  1283  dfbi3dc  1285  xordidc  1287  ax11v2  1698  ax11b  1704  equs5or  1708  nfsbxyt  1816  sbcomxyyz  1843  2exeu  1989  dimatis  2014  gencbvex  2594  gencbval  2596  elrab3t  2691  euind  2722  reu6  2724  reuind  2738  sbcan  2799  sbcralt  2828  sbcrext  2829  csbcomg  2867  csbiebt  2880  sbcnestgf  2891  sseq1  2960  ddifnel  3069  elin  3120  undif3ss  3192  uneqdifeqim  3302  disjpr2  3425  diftpsn3  3496  preqr1g  3528  nfopd  3557  unissel  3600  trel  3852  iinexgm  3899  copsex2t  3973  sowlin  4048  ordelon  4086  alxfr  4159  ralxfr  4164  rexxfr  4166  rabxfr  4168  reuhyp  4170  ordelsuc  4197  onsucelsucr  4199  onsucsssucr  4200  ordtriexmidlem  4208  onsucelsucexmidlem  4214  ordsucunielexmid  4216  regexmidlem1  4218  preleq  4233  eunex  4239  ordsuc  4241  nlimsucg  4242  onnmin  4244  tfi  4248  peano2  4261  opeliunxp  4338  posng  4355  sosng  4356  eqrelrdv2  4382  ideqg  4430  opeldmg  4483  relssres  4591  exse2  4642  brcodir  4655  xpidtr  4658  poltletr  4668  ssxpbm  4699  ssxp1  4700  ssxp2  4701  xpexr2m  4705  rnpropg  4743  elxp4  4751  elxp5  4752  dfco2a  4764  iota5  4830  iota2  4836  funssres  4885  funun  4887  fnsng  4890  fununi  4910  funimaexglem  4925  fneu  4946  fco  4999  fco2  5000  funssxp  5003  fssres2  5010  f1orescnv  5085  nffvd  5130  fnsnfv  5175  ssimaex  5177  funfvdm2  5180  dmfco  5184  fvco2  5185  fvmptss2  5190  respreima  5238  rexrn  5247  ralrn  5248  elrnrexdm  5249  ralrnmpt  5252  rexrnmpt  5253  ffvresb  5271  fcompt  5276  xpsng  5281  fprg  5289  fsnunres  5307  resfunexg  5325  funfvima3  5335  rexima  5337  ralima  5338  f1veqaeq  5351  f1ocnvfv1  5360  f1ocnvfv2  5361  fcofo  5367  foeqcnvco  5373  f1eqcocnv  5374  isoresbr  5392  isoini  5400  isoselem  5402  f1oiso  5408  riotabiia  5428  riota2f  5432  riota5f  5435  eloprabga  5533  ovmpt2x  5571  ovmpt2ga  5572  ovg  5581  oprssov  5584  caovcl  5597  caovimo  5636  f1opw2  5648  ofres  5667  resfunexgALT  5679  cofunexg  5680  iunexg  5688  offval3  5703  f2ndres  5729  elxp6  5738  releldm2  5753  oprabco  5780  1stconst  5784  2ndconst  5785  cnvf1o  5788  fo2ndf  5790  f1o2ndf1  5791  poxp  5794  mpt2xopoveq  5796  sprmpt2  5798  isprmpt2  5799  reldmtpos  5809  dftpos4  5819  tposf2  5824  iunon  5840  iordsmo  5853  tfrlem1  5864  tfrlemisucaccv  5880  tfrlemi1  5887  tfrexlem  5889  tfri3  5894  rdgivallem  5908  rdgon  5913  freccl  5932  oasuc  5983  omsuc  5990  nnaass  6003  nndi  6004  nnsucelsuc  6009  nntri1  6013  nntri3  6014  nnaordi  6017  nnaword  6020  nnmord  6026  nnm00  6038  swoer  6070  eqer  6074  0er  6076  relelec  6082  ectocl  6109  iinerm  6114  eroveu  6133  ecopovtrn  6139  ecopover  6140  ecopovsymg  6141  ecopovtrng  6142  ecopoverg  6143  th3qlem1  6144  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  ener  6195  fundmen  6222  cnven  6224  xpcomco  6236  xpdom2  6241  fopwdom  6246  ltpiord  6303  ltsopi  6304  mulclpi  6312  addasspig  6314  mulasspig  6316  distrpig  6317  addnidpig  6320  ltapig  6322  ltmpig  6323  indpi  6326  nnppipi  6327  enqdc1  6346  addcmpblnq  6351  mulcmpblnq  6352  ordpipqqs  6358  addassnqg  6366  mulcanenq  6369  distrnqg  6371  mulidnq  6373  recmulnqg  6375  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltaddnq  6390  ltexnqq  6391  halfnqq  6393  ltbtwnnqq  6398  archnqq  6400  prarloclemarch  6401  prarloclemarch2  6402  ltrnqg  6403  enq0tr  6417  enq0er  6418  nqnq0  6424  addcmpblnq0  6426  mulcmpblnq0  6427  mulcanenq0ec  6428  nnnq0lem1  6429  mulnnnq0  6433  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  nq0a0  6440  distrnq0  6442  addassnq0  6445  nq02m  6448  prcdnql  6467  prcunqu  6468  prubl  6469  prloc  6474  prarloclemlt  6476  prarloclemlo  6477  prarloc  6486  genplt2i  6493  genprndl  6504  genprndu  6505  genpdisj  6506  genpassl  6507  genpassu  6508  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocprlemeqgt  6515  nqprloc  6528  nqprl  6533  addnqprlemrl  6538  addnqprlemru  6539  appdivnq  6544  prmuloc  6547  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  distrlem4prl  6560  distrlem4pru  6561  1idprl  6566  1idpru  6567  ltpopr  6569  ltsopr  6570  ltaddpr  6571  ltexprlemupu  6578  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  addcanprleml  6588  ltaprg  6592  addextpr  6593  recexprlemdisj  6602  recexprlemloc  6603  recexprlem1ssl  6605  recexprlem1ssu  6606  aptiprleml  6611  aptiprlemu  6612  cauappcvgprlemcan  6616  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlemlim  6652  mulcmpblnrlemg  6668  ltsrprg  6675  mulasssrg  6686  distrsrg  6687  lttrsr  6690  ltposr  6691  ltsosr  6692  0idsr  6695  1idsr  6696  ltasrg  6698  recexgt0sr  6701  mulgt0sr  6704  mulextsr1lem  6706  archsr  6708  axmulass  6757  axdistr  6758  ax0id  6762  axcnre  6765  ltxrlt  6882  ltso  6893  muladd11  6943  readdcan  6950  cnegexlem1  6983  cnegexlem3  6985  cnegex  6986  addsubeq4  7023  subeq0  7033  renegcl  7068  mul2neg  7191  submul2  7192  ltleadd  7236  ltaddpos  7242  lt2sub  7250  le2sub  7251  lenegcon2  7257  recexre  7362  apirr  7389  apsym  7390  apneg  7395  apti  7406  recextlem1  7414  recexap  7416  mulap0  7417  divvalap  7435  rec11ap  7468  divdivdivap  7471  divmul24ap  7474  divmuleqap  7475  divadddivap  7485  conjmulap  7487  letrp1  7595  ltdivmul  7623  lerec2  7636  ledivdiv  7637  cju  7694  nn1suc  7714  nn2ge  7727  nnsub  7733  nndiv  7735  halfaddsub  7936  nn0addcl  7993  nn0mulcl  7994  elnn0nn  8000  nn0ge2m1nn  8018  znegcl  8052  zaddcllempos  8058  zaddcllemneg  8060  zaddcl  8061  ztri3or  8064  zltnle  8067  zltp1le  8074  zltlem1  8077  elz2  8088  zdceq  8092  zdclt  8094  zdivadd  8105  gtndiv  8111  prime  8113  zneo  8115  zeo  8119  peano2uz2  8121  uzind  8125  fzind  8129  eluzuzle  8257  uztrn  8265  eluzp1l  8273  peano2uzr  8304  uzaddcl  8305  indstr  8312  indstr2  8322  ublbneg  8324  divfnzn  8332  qmulz  8334  qaddcl  8346  qnegcl  8347  qapne  8350  qreccl  8351  irradd  8355  irrmul  8356  xrltnsym  8484  xrlttr  8486  xrltso  8487  xrlttri3  8488  xrre  8503  xrre2  8504  xrre3  8505  xltnegi  8518  ixxss1  8543  ixxss2  8544  ixxss12  8545  ubioog  8553  iccss2  8583  iccssioo2  8585  iccssico2  8586  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  divelunit  8640  lincmb01cmp  8641  iccf1o  8642  fztri3or  8673  uzsubsubfz  8681  fzsplit2  8684  fzdisj  8686  fzaddel  8692  fzsubel  8693  fzss1  8696  fzss2  8697  fznatpl1  8708  fzdifsuc  8713  fzrev  8716  fzrev2  8717  fzrev2i  8718  fzrev3  8719  elfzm11  8723  uzsplit  8724  fzm1  8732  fzneuz  8733  elfz2nn0  8743  elfz0addOLD  8750  elfz0fzfz0  8753  fz0fzelfz0  8754  uzsubfz0  8756  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  difelfzle  8762  difelfznle  8763  1fv  8766  fzon  8792  fzoss1  8797  fzouzdisj  8806  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  fzoaddel2  8819  fzosubel2  8821  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  zpnn0elfzo1  8834  fzosplitsnm1  8835  elfzom1p1elfzo  8840  ssfzo12bi  8851  ubmelm1fzo  8852  fzofzp1b  8854  elfzom1b  8855  elfzomelpfzo  8857  peano2fzor  8858  fzoshftral  8864  frec2uzzd  8867  frec2uzuzd  8869  frec2uzltd  8870  frec2uzlt2d  8871  frecuzrdgrrn  8875  frecuzrdgfn  8879  frecuzrdgsuc  8882  fzofig  8889  nn0ennn  8890  iseqfveq2  8905  iseqfeq2  8906  expivallem  8910  expival  8911  expinnval  8912  exp1  8915  expp1  8916  expnegap0  8917  expm1t  8937  expap0  8939  expadd  8951  expsubap  8956  leexp1a  8963  subsq  9011  subsq2  9012  binom2sub  9017  bernneq  9022  bernneq3  9024  expnlbnd  9026  crre  9085  rereb  9091  mulreap  9092  readd  9097  resub  9098  remullem  9099  imadd  9105  imsub  9106  cjadd  9112  ipcnval  9114  cjsub  9120  sqrt0  9213  cbvrald  9262  bdsepnft  9342  bj-om  9396  bj-nnen2lp  9414  strcollnft  9444  sscoll2  9448
  Copyright terms: Public domain W3C validator