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

Theorem adantl 266
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 265 . 2 ((𝜑𝜒) → 𝜓)
32ancoms 259 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  sylan2  274  anim12ii  329  simplbiim  373  sylan9bb  443  ad2antrl  467  ad2antll  468  im2anan9  540  bi2bian9  550  jaao  649  ordi  740  con1bidc  779  con1bdc  783  dfandc  789  stabtestimpdc  835  dcor  854  annimdc  856  ccase2  884  rnlem  894  simpr1  921  simpr2  922  simpr3  923  3ad2ant3  938  simprl1  960  simprl2  961  simprl3  962  simprr1  963  simprr2  964  simprr3  965  simpr1l  972  simpr1r  973  simpr2l  974  simpr2r  975  simpr3l  976  simpr3r  977  simpr11  999  simpr12  1000  simpr13  1001  simpr21  1002  simpr22  1003  simpr23  1004  simpr31  1005  simpr32  1006  simpr33  1007  falimd  1274  xorbin  1291  xor2dc  1297  biassdc  1302  dfbi3dc  1304  xordidc  1306  ax11v2  1717  ax11b  1723  equs5or  1727  nfsbxyt  1835  sbcomxyyz  1862  2exeu  2008  dimatis  2033  gencbvex  2617  gencbval  2619  rspcdva  2679  elrab3t  2720  euind  2751  reu6  2753  reuind  2767  sbcan  2828  sbcralt  2862  sbcrext  2863  csbcomg  2901  csbiebt  2914  sbcnestgf  2925  sseq1  2994  ddifnel  3103  elin  3154  undif3ss  3226  uneqdifeqim  3336  ifcldcd  3386  disjpr2  3462  diftpsn3  3533  preqr1g  3565  nfopd  3594  unissel  3637  trel  3889  iinexgm  3936  copsex2t  4010  sowlin  4085  efrirr  4118  ordelon  4148  alxfr  4221  ralxfr  4226  rexxfr  4228  rabxfr  4230  reuhyp  4232  ordelsuc  4259  onsucelsucr  4262  onsucsssucr  4263  onintonm  4271  ordtriexmidlem  4273  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  ordsucunielexmid  4284  regexmidlem1  4286  reg2exmidlema  4287  preleq  4307  eunex  4313  ordsuc  4315  nlimsucg  4318  onnmin  4320  wessep  4330  tfi  4333  peano2  4346  opeliunxp  4423  posng  4440  sosng  4441  eqrelrdv2  4467  ideqg  4515  opeldmg  4568  relssres  4676  exse2  4727  brcodir  4740  xpidtr  4743  poltletr  4753  ssxpbm  4784  ssxp1  4785  ssxp2  4786  xpexr2m  4790  rnpropg  4828  elxp4  4836  elxp5  4837  dfco2a  4849  iota5  4915  iota2  4921  funssres  4970  funun  4972  fnsng  4975  fununi  4995  funimaexglem  5010  fneu  5031  fco  5084  fco2  5085  funssxp  5088  fssres2  5095  f1orescnv  5170  nffvd  5215  fnsnfv  5260  ssimaex  5262  funfvdm2  5265  dmfco  5269  fvco2  5270  fvmptss2  5275  respreima  5323  rexrn  5332  ralrn  5333  elrnrexdm  5334  ralrnmpt  5337  rexrnmpt  5338  ffvresb  5356  fcompt  5361  xpsng  5366  fprg  5374  fsnunres  5392  resfunexg  5410  funfvima3  5420  rexima  5422  ralima  5423  f1veqaeq  5436  f1ocnvfv1  5445  f1ocnvfv2  5446  fcofo  5452  foeqcnvco  5458  f1eqcocnv  5459  isoresbr  5477  isoini  5485  isoselem  5487  f1oiso  5493  riotabiia  5513  riota2f  5517  riota5f  5520  eloprabga  5619  ovmpt2x  5657  ovmpt2ga  5658  ovg  5667  oprssov  5670  caovcl  5683  caovimo  5722  f1opw2  5734  ofres  5753  resfunexgALT  5765  cofunexg  5766  iunexg  5774  offval3  5789  f2ndres  5815  elxp6  5824  releldm2  5839  oprabco  5866  1stconst  5870  2ndconst  5871  cnvf1o  5874  fo2ndf  5876  f1o2ndf1  5877  poxp  5881  cnvoprab  5883  mpt2xopoveq  5886  sprmpt2  5888  isprmpt2  5889  reldmtpos  5899  dftpos4  5909  tposf2  5914  iunon  5930  iordsmo  5943  tfrlem1  5954  tfrlemisucaccv  5970  tfrlemi1  5977  tfrexlem  5979  tfri3  5984  rdgivallem  5999  rdgon  6004  freccl  6024  oasuc  6075  omsuc  6082  nnaass  6095  nndi  6096  nnsucelsuc  6101  nntri1  6105  nntri3  6106  nntri2or2  6107  nnsseleq  6110  nndifsnid  6111  nnaordi  6112  nnaword  6115  nnmord  6121  nnm00  6133  swoer  6165  eqer  6169  0er  6171  relelec  6177  ectocl  6204  iinerm  6209  eroveu  6228  ecopovtrn  6234  ecopover  6235  ecopovsymg  6236  ecopovtrng  6237  ecopoverg  6238  th3qlem1  6239  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  ener  6290  fundmen  6317  cnven  6319  xpcomco  6331  xpdom2  6336  fopwdom  6341  phplem4  6349  phplem4dom  6355  nndomo  6357  phplem4on  6360  fidceq  6361  fidifsnen  6362  fidifsnid  6363  dif1en  6368  fin0  6373  fin0or  6374  findcard2  6377  findcard2s  6378  diffisn  6381  ac6sfi  6383  onunsnss  6386  snon0  6387  eqsupti  6402  supsnti  6409  ordiso2  6415  cardcl  6419  isnumi  6420  carden2bex  6427  ltpiord  6475  ltsopi  6476  mulclpi  6484  addasspig  6486  mulasspig  6488  distrpig  6489  addnidpig  6492  ltapig  6494  ltmpig  6495  indpi  6498  nnppipi  6499  enqdc1  6518  addcmpblnq  6523  mulcmpblnq  6524  ordpipqqs  6530  addassnqg  6538  mulcanenq  6541  distrnqg  6543  mulidnq  6545  recmulnqg  6547  ltsonq  6554  ltanqg  6556  ltmnqg  6557  ltaddnq  6563  ltexnqq  6564  halfnqq  6566  ltbtwnnqq  6571  archnqq  6573  prarloclemarch  6574  prarloclemarch2  6575  ltrnqg  6576  enq0tr  6590  enq0er  6591  nqnq0  6597  addcmpblnq0  6599  mulcmpblnq0  6600  mulcanenq0ec  6601  nnnq0lem1  6602  mulnnnq0  6606  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  nq0a0  6613  distrnq0  6615  addassnq0  6618  nq02m  6621  prcdnql  6640  prcunqu  6641  prubl  6642  prloc  6647  prarloclemlt  6649  prarloclemlo  6650  prarloc  6659  genplt2i  6666  genprndl  6677  genprndu  6678  genpdisj  6679  genpassl  6680  genpassu  6681  addnqprllem  6683  addnqprulem  6684  addnqprl  6685  addnqpru  6686  addlocprlemeqgt  6688  nqprloc  6701  nqprl  6707  nqpru  6708  addnqprlemrl  6713  addnqprlemru  6714  appdivnq  6719  prmuloc  6722  mulnqprl  6724  mulnqpru  6725  mullocprlem  6726  mulnqprlemrl  6729  mulnqprlemru  6730  distrlem4prl  6740  distrlem4pru  6741  1idprl  6746  1idpru  6747  ltpopr  6751  ltsopr  6752  ltaddpr  6753  ltexprlemupu  6760  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemfl  6765  ltexprlemrl  6766  ltexprlemfu  6767  ltexprlemru  6768  addcanprleml  6770  ltaprg  6775  prplnqu  6776  addextpr  6777  recexprlemdisj  6786  recexprlemloc  6787  recexprlem1ssl  6789  recexprlem1ssu  6790  aptiprleml  6795  aptiprlemu  6796  caucvgprlemcanl  6800  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemopu  6804  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdfu  6810  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem1  6815  archrecpr  6820  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemopu  6827  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlemlim  6837  caucvgprprlemval  6844  caucvgprprlemnkltj  6845  caucvgprprlemnkeqj  6846  caucvgprprlemnbj  6849  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemdisj  6858  caucvgprprlemloc  6859  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  caucvgprprlemaddq  6864  caucvgprprlemlim  6867  mulcmpblnrlemg  6883  ltsrprg  6890  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltposr  6906  ltsosr  6907  0idsr  6910  1idsr  6911  ltasrg  6913  recexgt0sr  6916  mulgt0sr  6920  mulextsr1lem  6922  archsr  6924  srpospr  6925  prsradd  6928  prsrlt  6929  caucvgsrlemfv  6933  caucvgsrlemoffval  6938  caucvgsrlemoffcau  6940  caucvgsrlemoffgt1  6941  caucvgsrlemoffres  6942  caucvgsr  6944  ltrennb  6988  axmulass  7005  axdistr  7006  ax0id  7010  axcnre  7013  axcaucvglemval  7029  axcaucvglemcau  7030  axcaucvglemres  7031  ltxrlt  7144  ltso  7155  muladd11  7207  readdcan  7214  cnegexlem1  7249  cnegexlem3  7251  cnegex  7252  addsubeq4  7289  subeq0  7300  renegcl  7335  mul2neg  7467  submul2  7468  ltaddneg  7493  ltleadd  7515  ltaddpos  7521  lt2sub  7529  le2sub  7530  lenegcon2  7536  recexre  7643  apirr  7670  apsym  7671  apneg  7676  apti  7687  recextlem1  7706  recexap  7708  mulap0  7709  divvalap  7727  rec11ap  7761  divdivdivap  7764  divmul24ap  7767  divmuleqap  7768  divadddivap  7778  conjmulap  7780  letrp1  7889  ltdivmul  7917  lerec2  7930  ledivdiv  7931  cju  7989  nn1suc  8009  nn2ge  8022  nnsub  8028  nndiv  8030  halfaddsub  8216  nn0addcl  8274  nn0mulcl  8275  elnn0nn  8281  nn0ge2m1nn  8299  znegcl  8333  zaddcllempos  8339  zaddcllemneg  8341  zaddcl  8342  ztri3or  8345  zltnle  8348  nzadd  8354  zltp1le  8356  zltlem1  8359  elz2  8370  zdceq  8374  zdclt  8376  zdivadd  8387  gtndiv  8393  prime  8396  zneo  8398  zeo  8402  peano2uz2  8404  uzind  8408  fzind  8412  eluzuzle  8577  uztrn  8585  eluzp1l  8593  peano2uzr  8624  uzaddcl  8625  indstr  8632  indstr2  8643  ublbneg  8645  divfnzn  8653  qmulz  8655  qaddcl  8667  qnegcl  8668  qapne  8671  qreccl  8674  irradd  8678  irrmul  8679  divlt1lt  8748  divle1le  8749  ledivge1le  8750  nnledivrp  8784  nn0ledivnn  8785  addlelt  8786  xrltnsym  8815  xrlttr  8817  xrltso  8818  xrlttri3  8819  xrre  8834  xrre2  8835  xrre3  8836  xltnegi  8849  ixxss1  8874  ixxss2  8875  ixxss12  8876  ubioog  8884  iccss2  8914  iccssioo2  8916  iccssico2  8917  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  divelunit  8971  lincmb01cmp  8972  iccf1o  8973  zltaddlt1le  8975  fztri3or  9005  uzsubsubfz  9013  fzsplit2  9016  fzdisj  9018  fzaddel  9024  fzsubel  9025  fzss1  9028  fzss2  9029  fznatpl1  9040  fzdifsuc  9045  fzrev  9048  fzrev2  9049  fzrev2i  9050  fzrev3  9051  elfzm11  9055  uzsplit  9056  fzm1  9064  fzneuz  9065  elfz2nn0  9075  elfz0addOLD  9082  elfz0fzfz0  9085  fz0fzelfz0  9086  uzsubfz0  9088  fz0fzdiffz0  9089  elfzmlbmOLD  9091  elfzmlbp  9092  difelfzle  9094  difelfznle  9095  1fv  9098  fzon  9124  fzoss1  9129  fzouzdisj  9138  fzo1fzo0n0  9141  elfzo0z  9142  fzofzim  9146  fzoaddel2  9151  fzosubel2  9153  eluzgtdifelfzo  9155  elfzodifsumelfzo  9159  zpnn0elfzo1  9166  fzosplitsnm1  9167  elfzom1p1elfzo  9172  ssfzo12bi  9183  ubmelm1fzo  9184  fzofzp1b  9186  elfzom1b  9187  elfzomelpfzo  9189  peano2fzor  9190  fzoshftral  9196  fvinim0ffz  9198  subfzo0  9199  qtri3or  9200  qltnle  9203  qdceq  9204  qbtwnzlemshrink  9206  rebtwn2zlemshrink  9210  qbtwnxr  9214  qavgle  9215  flqlt  9233  flqmulnn0  9249  flqeqceilz  9268  intfracq  9270  flqdiv  9271  zmod1congr  9291  zmodcl  9294  zmodfz  9296  zmodfzo  9297  zmodid2  9302  zmodidfzo  9303  mulp1mod1  9315  modqmuladd  9316  modqmuladdnn0  9318  modqm1p1mod0  9325  modifeq2int  9336  modaddmodup  9337  modaddmodlo  9338  modfzo0difsn  9345  modsumfzodifsn  9346  frec2uzzd  9350  frec2uzuzd  9352  frec2uzltd  9353  frec2uzlt2d  9354  frecuzrdgrrn  9358  frecuzrdgfn  9362  frecuzrdgsuc  9365  fzofig  9372  nn0ennn  9373  iseqfveq2  9392  iseqfeq2  9393  iseqshft2  9396  iserf  9397  iserfre  9398  monoord2  9400  isermono  9401  iseqsplit  9402  iseqcaopr3  9404  iseqcaopr2  9405  iseradd  9407  isersub  9408  iseqid3s  9410  iser0  9415  iser0f  9416  serige0  9417  serile  9418  expivallem  9421  expival  9422  expinnval  9423  exp1  9426  expp1  9427  expnegap0  9428  expm1t  9448  expap0  9450  expadd  9462  expsubap  9468  leexp1a  9475  subsq  9525  subsq2  9526  binom2sub  9531  bernneq  9537  bernneq3  9539  expnlbnd  9541  facnn  9595  fac0  9596  fac1  9597  facp1  9598  facnn2  9602  faccl  9603  facdiv  9606  facwordi  9608  faclbnd  9609  faclbnd3  9611  faclbnd6  9612  facavg  9614  bcval  9617  bcval4  9620  bccmpl  9622  ibcval5  9631  bcn2  9632  bccl  9635  shftfib  9652  shftfn  9653  shftval3  9656  crre  9685  rereb  9691  mulreap  9692  readd  9697  resub  9698  remullem  9699  imadd  9705  imsub  9706  cjadd  9712  ipcnval  9714  cjsub  9720  caucvgrelemcau  9807  cvg1nlemcau  9811  rexuz3  9817  recvguniq  9822  sqrt0  9831  resqrexlemfp1  9836  resqrexlemover  9837  resqrexlemcalc3  9843  resqrexlemcvg  9846  resqrexlemgt0  9847  resqrexlemga  9850  sqrtmul  9862  sqrtdiv  9869  sqabsadd  9882  sqabssub  9883  absexp  9906  abs2dif2  9934  fzomaxdiflem  9939  cau3lem  9941  qdenre  10029  climconst  10042  2clim  10053  climshftlemg  10054  climres  10055  climshft2  10058  addcn2  10062  subcn2  10063  mulcn2  10064  climcn1lem  10070  climadd  10077  climmul  10078  climsub  10079  clim2iser  10088  clim2iser2  10089  iisermulc2  10091  iserile  10093  climserile  10096  climcau  10097  climcvg1nlem  10099  climcaucn  10101  serif0  10102  dvdsval2  10111  dvdsval3  10112  nndivdvds  10114  nndivides  10115  dvds0lem  10118  negdvdsb  10124  dvdsnegb  10125  dvdsabsb  10127  modmulconst  10139  dvds2ln  10140  dvds2add  10141  dvds2sub  10142  dvdstr  10144  dvdsadd2b  10154  dvdsabseq  10159  divconjdvds  10161  dvdsssfz1  10164  alzdvds  10166  fzm1ndvds  10168  fzocongeq  10170  dvdsfac  10172  odd2np1lem  10183  odd2np1  10184  even2n  10185  mod2eq1n2dvds  10191  oddge22np1  10193  evennn02n  10194  evennn2n  10195  2tp1odd  10196  mulsucdiv2z  10197  2teven  10199  ltoddhalfle  10205  halfleoddlt  10206  opeo  10209  omeo  10210  m1expo  10212  nn0o1gt2  10217  nn0ob  10220  divalglemnn  10230  divalg2  10238  divalgmod  10239  modremain  10241  flodddiv4  10246  flodddiv4lt  10248  pw2dvdslemn  10253  oddpwdc  10262  nn0seqcvgd  10263  ialgrlem1st  10264  algcvgblem  10271  ialgcvga  10273  ialgfx  10274  cbvrald  10314  bdsepnft  10394  bj-om  10448  bj-nnen2lp  10466  strcollnft  10496  sscoll2  10500
  Copyright terms: Public domain W3C validator