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

Theorem adantl 271
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 270 . 2 ((𝜑𝜒) → 𝜓)
32ancoms 264 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  sylan2  280  anim12ii  335  simplbiim  379  sylan9bb  450  ad2antrl  474  ad2antll  475  im2anan9  563  bi2bian9  573  jaao  672  ordi  763  con1bidc  804  con1bdc  808  dfandc  814  stabtestimpdc  860  dcor  879  annimdc  881  orandc  883  ccase2  910  rnlem  920  simpr1  947  simpr2  948  simpr3  949  3ad2ant3  964  simprl1  986  simprl2  987  simprl3  988  simprr1  989  simprr2  990  simprr3  991  simpr1l  998  simpr1r  999  simpr2l  1000  simpr2r  1001  simpr3l  1002  simpr3r  1003  simpr11  1025  simpr12  1026  simpr13  1027  simpr21  1028  simpr22  1029  simpr23  1030  simpr31  1031  simpr32  1032  simpr33  1033  falimd  1302  xorbin  1318  xor2dc  1324  biassdc  1329  dfbi3dc  1331  xordidc  1333  ax11v2  1745  ax11b  1751  equs5or  1755  nfsbxyt  1864  sbcomxyyz  1891  2exeu  2037  dimatis  2062  gencbvex  2659  gencbval  2661  elrab3t  2761  euind  2793  reu6  2795  reuind  2809  sbcan  2870  sbcralt  2904  sbcrext  2905  csbcomg  2943  csbiebt  2956  sbcnestgf  2968  sseq1  3036  ddifnel  3120  elin  3172  undif3ss  3249  uneqdifeqim  3355  ifcldadc  3406  ifeq1dadc  3407  ifbothdadc  3408  ifcldcd  3412  disjpr2  3489  diftpsn3  3561  preqr1g  3593  nfopd  3622  unissel  3665  trel  3918  iinexgm  3965  exmidundif  4009  copsex2t  4046  sowlin  4121  efrirr  4154  ordelon  4184  alxfr  4257  ralxfr  4262  rexxfr  4264  rabxfr  4266  reuhyp  4268  ordelsuc  4295  onsucelsucr  4298  onsucsssucr  4299  onintonm  4307  ordtriexmidlem  4309  ordtri2or2exmidlem  4315  onsucelsucexmidlem  4318  ordsucunielexmid  4320  regexmidlem1  4322  reg2exmidlema  4323  preleq  4344  eunex  4350  ordsuc  4352  nlimsucg  4355  onnmin  4357  wessep  4366  tfi  4370  peano2  4383  posng  4478  sosng  4479  eqrelrdv2  4505  ideqg  4555  opeldmg  4609  relssres  4717  exse2  4773  brcodir  4786  xpidtr  4789  poltletr  4799  ssxpbm  4832  ssxp1  4833  ssxp2  4834  xpexr2m  4838  rnpropg  4876  elxp4  4884  elxp5  4885  dfco2a  4897  iota5  4966  iota2  4972  funssres  5021  funun  5023  fnsng  5026  fununi  5047  funimaexglem  5062  fneu  5083  fco  5140  fco2  5141  funssxp  5144  fssres2  5151  f0rn0  5168  f1orescnv  5232  nffvd  5280  fnsnfv  5326  ssimaex  5328  funfvdm2  5331  dmfco  5335  fvco2  5336  fvmptss2  5342  respreima  5390  rexrn  5399  ralrn  5400  elrnrexdm  5401  ralrnmpt  5404  rexrnmpt  5405  ffvresb  5424  fcompt  5430  xpsng  5435  fprg  5443  fsnunres  5461  resfunexg  5479  funfvima3  5489  rexima  5495  ralima  5496  f1veqaeq  5509  f1ocnvfv1  5517  f1ocnvfv2  5518  fcofo  5524  foeqcnvco  5530  f1eqcocnv  5531  isoresbr  5549  isoini  5558  isoselem  5560  f1oiso  5566  riotabiia  5586  riota2f  5590  riota5f  5593  eloprabga  5692  ovmpt2x  5730  ovmpt2ga  5731  ovg  5740  oprssov  5743  caovcl  5756  caovimo  5795  f1opw2  5807  ofres  5826  resfunexgALT  5838  cofunexg  5839  iunexg  5847  offval3  5862  f2ndres  5888  elxp6  5897  releldm2  5912  oprabco  5939  1stconst  5943  2ndconst  5944  cnvf1o  5947  fo2ndf  5949  f1o2ndf1  5950  poxp  5954  cnvoprab  5956  mpt2xopoveq  5959  sprmpt2  5961  isprmpt2  5962  reldmtpos  5972  dftpos4  5982  tposf2  5987  iunon  6003  iordsmo  6016  tfrlem1  6027  tfrlemisucaccv  6044  tfrlemi1  6051  tfrexlem  6053  tfr1onlemsucaccv  6060  tfri1dALT  6070  tfrcllemsucaccv  6073  tfri3  6086  rdgivallem  6100  rdgon  6105  frecabcl  6118  freccllem  6121  frecfcllem  6123  frecsuclem  6125  oasuc  6179  oawordriexmid  6185  omsuc  6187  nnaass  6200  nndi  6201  nnsucelsuc  6206  nnsucuniel  6210  nntri1  6211  nntri3  6212  nntri2or2  6213  nnsseleq  6216  dcdifsnid  6217  nnaordi  6219  nnaword  6222  nnmord  6228  nnm00  6240  swoer  6272  eqer  6276  0er  6278  relelec  6284  ectocl  6311  iinerm  6316  eroveu  6335  ecopovtrn  6341  ecopover  6342  ecopovsymg  6343  ecopovtrng  6344  ecopoverg  6345  th3qlem1  6346  ecovass  6353  ecoviass  6354  ecovdi  6355  ecovidi  6356  pmss12g  6384  pmresg  6385  mapss  6400  fdiagfn  6401  ener  6448  fundmen  6475  cnven  6477  1domsn  6487  xpcomco  6494  xpdom2  6499  fopwdom  6504  dom0  6506  xpf1o  6512  mapen  6514  mapdom1g  6515  mapxpen  6516  xpmapenlem  6517  phplem4  6523  phplem4dom  6530  nndomo  6532  phplem4on  6535  fidceq  6537  fidifsnen  6538  infiexmid  6545  dif1en  6547  dif1enen  6548  fin0  6553  fin0or  6554  findcard2  6557  findcard2s  6558  diffisn  6561  infnfi  6563  ac6sfi  6566  infm  6572  en2eqpr  6575  onunsnss  6579  unsnfidcex  6582  unsnfidcel  6583  undifdcss  6585  xpfi  6590  fisseneq  6592  ssfirab  6593  snon0  6595  relcnvfi  6600  f1finf1o  6605  en1eqsn  6606  sbthlemi3  6612  sbthlemi6  6615  isbth  6620  eqsupti  6635  supsnti  6644  cnvti  6658  ordiso2  6672  djueq12  6676  djuf1olem  6689  djulclb  6691  djuun  6704  djuss  6705  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  updjudhf  6714  updjudhcoinlf  6715  updjudhcoinrg  6716  updjud  6717  enomnilem  6738  finomni  6740  exmidomniim  6741  exmidomni  6742  nnnninf  6750  cardcl  6753  isnumi  6754  carden2bex  6761  exmidfodomrlemim  6771  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  ltpiord  6822  ltsopi  6823  mulclpi  6831  addasspig  6833  mulasspig  6835  distrpig  6836  addnidpig  6839  ltapig  6841  ltmpig  6842  indpi  6845  nnppipi  6846  enqdc1  6865  addcmpblnq  6870  mulcmpblnq  6871  ordpipqqs  6877  addassnqg  6885  mulcanenq  6888  distrnqg  6890  mulidnq  6892  recmulnqg  6894  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltaddnq  6910  ltexnqq  6911  halfnqq  6913  ltbtwnnqq  6918  archnqq  6920  prarloclemarch  6921  prarloclemarch2  6922  ltrnqg  6923  enq0tr  6937  enq0er  6938  nqnq0  6944  addcmpblnq0  6946  mulcmpblnq0  6947  mulcanenq0ec  6948  nnnq0lem1  6949  mulnnnq0  6953  nqnq0a  6957  nqnq0m  6958  nq0m0r  6959  nq0a0  6960  distrnq0  6962  addassnq0  6965  nq02m  6968  prcdnql  6987  prcunqu  6988  prubl  6989  prloc  6994  prarloclemlt  6996  prarloclemlo  6997  prarloc  7006  genplt2i  7013  genprndl  7024  genprndu  7025  genpdisj  7026  genpassl  7027  genpassu  7028  addnqprllem  7030  addnqprulem  7031  addnqprl  7032  addnqpru  7033  addlocprlemeqgt  7035  nqprloc  7048  nqprl  7054  nqpru  7055  addnqprlemrl  7060  addnqprlemru  7061  appdivnq  7066  prmuloc  7069  mulnqprl  7071  mulnqpru  7072  mullocprlem  7073  mulnqprlemrl  7076  mulnqprlemru  7077  distrlem4prl  7087  distrlem4pru  7088  1idprl  7093  1idpru  7094  ltpopr  7098  ltsopr  7099  ltaddpr  7100  ltexprlemupu  7107  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprleml  7117  ltaprg  7122  prplnqu  7123  addextpr  7124  recexprlemdisj  7133  recexprlemloc  7134  recexprlem1ssl  7136  recexprlem1ssu  7137  aptiprleml  7142  aptiprlemu  7143  caucvgprlemcanl  7147  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  archrecpr  7167  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlemlim  7184  caucvgprprlemval  7191  caucvgprprlemnkltj  7192  caucvgprprlemnkeqj  7193  caucvgprprlemnbj  7196  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemdisj  7205  caucvgprprlemloc  7206  caucvgprprlemexbt  7209  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  caucvgprprlemlim  7214  mulcmpblnrlemg  7230  ltsrprg  7237  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltposr  7253  ltsosr  7254  0idsr  7257  1idsr  7258  ltasrg  7260  recexgt0sr  7263  mulgt0sr  7267  mulextsr1lem  7269  archsr  7271  srpospr  7272  prsradd  7275  prsrlt  7276  caucvgsrlemfv  7280  caucvgsrlemoffval  7285  caucvgsrlemoffcau  7287  caucvgsrlemoffgt1  7288  caucvgsrlemoffres  7289  caucvgsr  7291  ltrennb  7335  axmulass  7352  axdistr  7353  ax0id  7357  axcnre  7360  axcaucvglemval  7376  axcaucvglemcau  7377  axcaucvglemres  7378  ltxrlt  7496  ltso  7507  muladd11  7559  readdcan  7566  cnegexlem1  7601  cnegexlem3  7603  cnegex  7604  addsubeq4  7641  subeq0  7652  renegcl  7687  negf1o  7804  mul2neg  7820  submul2  7821  ltaddneg  7846  ltleadd  7868  ltaddpos  7874  lt2sub  7882  le2sub  7883  lenegcon2  7889  recexre  7996  apirr  8023  apsym  8024  apneg  8029  apti  8040  recextlem1  8059  recexap  8061  mulap0  8062  divvalap  8080  rec11ap  8116  divdivdivap  8119  divmul24ap  8122  divmuleqap  8123  divadddivap  8133  conjmulap  8135  letrp1  8244  ltdivmul  8272  lerec2  8285  ledivdiv  8286  lbinf  8344  suprubex  8347  suprlubex  8348  suprleubex  8350  negiso  8351  cju  8356  nn1suc  8376  nn2ge  8389  nnsub  8395  nndiv  8397  halfaddsub  8583  nn0addcl  8641  nn0mulcl  8642  elnn0nn  8648  nn0ge2m1nn  8666  znegcl  8714  zaddcllempos  8720  zaddcllemneg  8722  zaddcl  8723  ztri3or  8726  zltnle  8729  nzadd  8735  zltp1le  8737  zltlem1  8740  elz2  8751  zdceq  8755  zdclt  8757  zdivadd  8768  gtndiv  8774  suprzclex  8777  prime  8778  zneo  8780  zeo  8784  peano2uz2  8786  uzind  8790  fzind  8794  eluzuzle  8959  uztrn  8967  eluzp1l  8975  peano2uzr  9005  uzaddcl  9006  indstr  9013  infrenegsupex  9014  supinfneg  9015  infsupneg  9016  supminfex  9017  indstr2  9028  ublbneg  9030  divfnzn  9038  qmulz  9040  qaddcl  9052  qnegcl  9053  qapne  9056  qreccl  9059  irradd  9063  irrmul  9064  divlt1lt  9133  divle1le  9134  ledivge1le  9135  nnledivrp  9169  nn0ledivnn  9170  addlelt  9171  xrltnsym  9195  xrlttr  9197  xrltso  9198  xrlttri3  9199  xrre  9214  xrre2  9215  xrre3  9216  xltnegi  9229  ixxss1  9254  ixxss2  9255  ixxss12  9256  ubioog  9264  iccss2  9294  iccssioo2  9296  iccssico2  9297  iccshftr  9343  iccshftl  9345  iccdil  9347  icccntr  9349  divelunit  9351  lincmb01cmp  9352  iccf1o  9353  zltaddlt1le  9355  fztri3or  9385  uzsubsubfz  9393  fzsplit2  9396  fzdisj  9398  fzaddel  9404  fzsubel  9405  fzss1  9408  fzss2  9409  fznatpl1  9420  fzdifsuc  9425  fzrev  9428  fzrev2  9429  fzrev2i  9430  fzrev3  9431  elfzm11  9435  uzsplit  9436  fzm1  9444  fzneuz  9445  elfz2nn0  9456  elfz0fzfz0  9465  fz0fzelfz0  9466  uzsubfz0  9468  fz0fzdiffz0  9469  elfzmlbp  9471  difelfzle  9473  difelfznle  9474  1fv  9478  fzon  9505  fzoss1  9510  fzouzdisj  9519  fzo1fzo0n0  9522  elfzo0z  9523  fzofzim  9527  fzoaddel2  9532  fzosubel2  9534  eluzgtdifelfzo  9536  elfzodifsumelfzo  9540  zpnn0elfzo1  9547  fzosplitsnm1  9548  elfzom1p1elfzo  9553  ssfzo12bi  9564  ubmelm1fzo  9565  fzofzp1b  9567  elfzom1b  9568  elfzomelpfzo  9570  peano2fzor  9571  fzoshftral  9577  exfzdc  9579  fvinim0ffz  9580  subfzo0  9581  qtri3or  9582  qltnle  9585  qdceq  9586  exbtwnzlemshrink  9588  rebtwn2zlemshrink  9593  qbtwnxr  9597  qavgle  9598  flqlt  9618  flqmulnn0  9634  flqeqceilz  9653  intfracq  9655  flqdiv  9656  zmod1congr  9676  zmodcl  9679  zmodfz  9681  zmodfzo  9682  zmodid2  9687  zmodidfzo  9688  mulp1mod1  9700  modqmuladd  9701  modqmuladdnn0  9703  modqm1p1mod0  9710  modifeq2int  9721  modaddmodup  9722  modaddmodlo  9723  modfzo0difsn  9730  modsumfzodifsn  9731  frec2uzuzd  9737  frec2uzltd  9738  frec2uzlt2d  9739  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgfunlem  9754  frecuzrdgsuctlem  9758  fzofig  9767  nn0ennn  9768  iseqvalt  9790  iseqfveq2  9803  iseqfeq2  9804  iseqshft2  9807  iserf  9808  iserfre  9809  monoord2  9811  isermono  9812  iseqsplit  9813  iseqcaopr3  9815  iseqcaopr2  9816  iseqf1olemqk  9828  iseqf1olemqsumkj  9832  iseqf1olemqsumk  9833  iseqf1olemqsum  9834  iseqf1olemstep  9835  iseqf1olemp  9836  iseqf1oleml  9837  iseqf1o  9838  iseradd  9839  isersub  9840  iseqid3s  9842  iseqid2  9844  iser0  9848  iser0f  9849  serige0  9851  serile  9852  expivallem  9855  expival  9856  expinnval  9857  exp1  9860  expp1  9861  expnegap0  9862  expm1t  9882  expap0  9884  expadd  9896  expsubap  9902  leexp1a  9909  subsq  9959  subsq2  9960  binom2sub  9965  bernneq  9971  bernneq3  9973  expnlbnd  9975  facnn  10032  fac0  10033  fac1  10034  facp1  10035  facnn2  10039  faccl  10040  facdiv  10043  facwordi  10045  faclbnd  10046  faclbnd3  10048  faclbnd6  10049  facavg  10051  bcval  10054  bcval4  10057  bccmpl  10059  ibcval5  10068  bcn2  10069  bccl  10072  hashinfuni  10082  hashennnuni  10084  hashfiv01gt1  10087  focdmex  10092  fihasheqf1oi  10093  fihashf1rn  10094  filtinf  10097  hashnncl  10101  hashunsng  10112  hashprg  10113  hashdifsn  10124  hashdifpr  10125  hashfzp1  10129  hashxp  10131  zfz1isolemiso  10141  zfz1isolem1  10142  zfz1iso  10143  iseqcoll  10144  shftfib  10154  shftfn  10155  shftval3  10158  crre  10187  rereb  10193  mulreap  10194  readd  10199  resub  10200  remullem  10201  imadd  10207  imsub  10208  cjadd  10214  ipcnval  10216  cjsub  10222  caucvgrelemcau  10309  cvg1nlemcau  10313  rexuz3  10319  recvguniq  10324  sqrt0  10333  resqrexlemfp1  10338  resqrexlemover  10339  resqrexlemcalc3  10345  resqrexlemcvg  10348  resqrexlemgt0  10349  resqrexlemga  10352  sqrtmul  10364  sqrtdiv  10371  sqabsadd  10384  sqabssub  10385  absexp  10408  abs2dif2  10436  fzomaxdiflem  10441  cau3lem  10443  qdenre  10531  maxleim  10534  maxabs  10538  maxleast  10542  rexanre  10549  fimaxre2  10553  negfi  10554  minmax  10556  climconst  10573  2clim  10584  climshftlemg  10585  climres  10586  climshft2  10589  addcn2  10593  subcn2  10594  mulcn2  10595  climcn1lem  10601  climadd  10608  climmul  10609  climsub  10610  clim2iser  10619  clim2iser2  10620  iisermulc2  10622  iserile  10624  climserile  10627  climcau  10628  climcvg1nlem  10630  climcaucn  10632  serif0  10633  isumrblem  10657  fisumcvg  10658  isummolem3  10661  isummolem2a  10662  zisum  10665  iisum  10666  fisum  10667  sum0  10668  isumz  10669  fisumss  10672  isumss2  10673  fisumcvg2  10674  fsumcl2lem  10677  dvdsval2  10681  dvdsval3  10682  nndivdvds  10684  nndivides  10685  dvds0lem  10688  negdvdsb  10694  dvdsnegb  10695  dvdsabsb  10697  zdvdsdc  10699  modmulconst  10710  dvds2ln  10711  dvds2add  10712  dvds2sub  10713  dvdstr  10715  dvdsadd2b  10725  dvdsabseq  10730  divconjdvds  10732  dvdsssfz1  10735  alzdvds  10737  fzm1ndvds  10739  fzocongeq  10741  dvdsfac  10743  odd2np1lem  10754  odd2np1  10755  even2n  10756  mod2eq1n2dvds  10761  oddge22np1  10763  evennn02n  10764  evennn2n  10765  2tp1odd  10766  mulsucdiv2z  10767  2teven  10769  ltoddhalfle  10775  halfleoddlt  10776  opeo  10779  omeo  10780  m1expo  10782  nn0o1gt2  10787  nn0ob  10790  divalglemnn  10800  divalg2  10808  divalgmod  10809  modremain  10811  flodddiv4  10816  flodddiv4lt  10818  gcdmndc  10822  zsupcl  10825  zssinfcl  10826  infssuzex  10827  infssuzledc  10828  infssuzcldc  10829  dvdsbnd  10830  gcddvds  10837  dvdslegcd  10838  gcdcl  10840  gcd0id  10852  gcdneg  10855  gcdaddm  10857  modgcd  10864  bezoutlemzz  10873  bezoutlemaz  10874  bezoutlembz  10875  bezoutlemsup  10880  dfgcd3  10881  dfgcd2  10885  dvdsmulgcd  10896  sqgcd  10900  dvdssq  10902  nn0seqcvgd  10905  ialgrlem1st  10906  algcvgblem  10913  ialgcvga  10915  ialgfx  10916  eucalgf  10919  eucalginv  10920  lcmmndc  10926  lcmval  10927  lcmcllem  10931  lcmledvds  10934  lcmneg  10938  lcmgcdlem  10941  lcmgcd  10942  lcmdvds  10943  lcmid  10944  lcmass  10949  coprmgcdb  10952  qredeq  10960  qredeu  10961  divgcdcoprm0  10965  divgcdcoprmex  10966  cncongr1  10967  cncongr2  10968  isprm3  10982  prmind2  10984  nprm  10987  dvdsnprmd  10989  sqnprm  10999  exprmfct  11001  prmdvdsfz  11002  divgcdodd  11004  prmdvdsexp  11009  prmdvdsexpr  11011  prmfac1  11013  rpexp  11014  pw2dvdslemn  11025  oddpwdc  11034  sqne2sq  11037  divnumden  11056  divdenle  11057  nn0gcdsq  11060  zgcdsq  11061  qden1elz  11065  nn0sqrtelqelz  11066  phivalfi  11070  hashdvds  11079  phiprmpw  11080  crth  11082  phimullem  11083  hashgcdeq  11086  xpct  11091  znnen  11093  cbvrald  11133  bdsepnft  11223  bj-om  11277  bj-nnen2lp  11294  strcollnft  11324  sscoll2  11328  nnpredcl  11335  nnsf  11340  peano4nninf  11341  peano3nninf  11342  nninfalllem1  11344  nninfsellemdc  11347  nninfsellemsuc  11349  nninfsellemqall  11352  nninfsellemeqinf  11353  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator