ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantl Structured version   GIF 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  6416  enq0er  6417  nqnq0  6423  addcmpblnq0  6425  mulcmpblnq0  6426  mulcanenq0ec  6427  nnnq0lem1  6428  mulnnnq0  6432  nqnq0a  6436  nqnq0m  6437  nq0m0r  6438  nq0a0  6439  distrnq0  6441  addassnq0  6444  nq02m  6447  prcdnql  6466  prcunqu  6467  prubl  6468  prloc  6473  prarloclemlt  6475  prarloclemlo  6476  prarloc  6485  genplt2i  6492  genprndl  6503  genprndu  6504  genpdisj  6505  genpassl  6506  genpassu  6507  addnqprllem  6509  addnqprulem  6510  addnqprl  6511  addnqpru  6512  addlocprlemeqgt  6514  nqprloc  6527  nqprl  6532  addnqprlemrl  6537  addnqprlemru  6538  appdivnq  6543  prmuloc  6546  mulnqprl  6548  mulnqpru  6549  mullocprlem  6550  distrlem4prl  6559  distrlem4pru  6560  1idprl  6565  1idpru  6566  ltpopr  6568  ltsopr  6569  ltaddpr  6570  ltexprlemupu  6577  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemfl  6582  ltexprlemrl  6583  ltexprlemfu  6584  ltexprlemru  6585  addcanprleml  6587  ltaprg  6591  addextpr  6592  recexprlemdisj  6601  recexprlemloc  6602  recexprlem1ssl  6604  recexprlem1ssu  6605  aptiprleml  6610  aptiprlemu  6611  cauappcvgprlemcan  6615  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  mulcmpblnrlemg  6648  ltsrprg  6655  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltposr  6671  ltsosr  6672  0idsr  6675  1idsr  6676  ltasrg  6678  recexgt0sr  6681  mulgt0sr  6684  mulextsr1lem  6686  archsr  6688  axmulass  6737  axdistr  6738  ax0id  6742  axcnre  6745  ltxrlt  6862  ltso  6873  muladd11  6923  readdcan  6930  cnegexlem1  6963  cnegexlem3  6965  cnegex  6966  addsubeq4  7003  subeq0  7013  renegcl  7048  mul2neg  7171  submul2  7172  ltleadd  7216  ltaddpos  7222  lt2sub  7230  le2sub  7231  lenegcon2  7237  recexre  7342  apirr  7369  apsym  7370  apneg  7375  apti  7386  recextlem1  7394  recexap  7396  mulap0  7397  divvalap  7415  rec11ap  7448  divdivdivap  7451  divmul24ap  7454  divmuleqap  7455  divadddivap  7465  conjmulap  7467  letrp1  7575  ltdivmul  7603  lerec2  7616  ledivdiv  7617  cju  7674  nn1suc  7694  nn2ge  7707  nnsub  7713  nndiv  7715  halfaddsub  7916  nn0addcl  7973  nn0mulcl  7974  elnn0nn  7980  nn0ge2m1nn  7998  znegcl  8032  zaddcllempos  8038  zaddcllemneg  8040  zaddcl  8041  ztri3or  8044  zltnle  8047  zltp1le  8054  zltlem1  8057  elz2  8068  zdceq  8072  zdclt  8074  zdivadd  8085  gtndiv  8091  prime  8093  zneo  8095  zeo  8099  peano2uz2  8101  uzind  8105  fzind  8109  eluzuzle  8237  uztrn  8245  eluzp1l  8253  peano2uzr  8284  uzaddcl  8285  indstr  8292  indstr2  8302  ublbneg  8304  divfnzn  8312  qmulz  8314  qaddcl  8326  qnegcl  8327  qapne  8330  qreccl  8331  irradd  8335  irrmul  8336  xrltnsym  8464  xrlttr  8466  xrltso  8467  xrlttri3  8468  xrre  8483  xrre2  8484  xrre3  8485  xltnegi  8498  ixxss1  8523  ixxss2  8524  ixxss12  8525  ubioog  8533  iccss2  8563  iccssioo2  8565  iccssico2  8566  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  divelunit  8620  lincmb01cmp  8621  iccf1o  8622  fztri3or  8653  uzsubsubfz  8661  fzsplit2  8664  fzdisj  8666  fzaddel  8672  fzsubel  8673  fzss1  8676  fzss2  8677  fznatpl1  8688  fzdifsuc  8693  fzrev  8696  fzrev2  8697  fzrev2i  8698  fzrev3  8699  elfzm11  8703  uzsplit  8704  fzm1  8712  fzneuz  8713  elfz2nn0  8723  elfz0addOLD  8730  elfz0fzfz0  8733  fz0fzelfz0  8734  uzsubfz0  8736  fz0fzdiffz0  8737  elfzmlbmOLD  8739  elfzmlbp  8740  difelfzle  8742  difelfznle  8743  1fv  8746  fzon  8772  fzoss1  8777  fzouzdisj  8786  fzo1fzo0n0  8789  elfzo0z  8790  fzofzim  8794  fzoaddel2  8799  fzosubel2  8801  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  zpnn0elfzo1  8814  fzosplitsnm1  8815  elfzom1p1elfzo  8820  ssfzo12bi  8831  ubmelm1fzo  8832  fzofzp1b  8834  elfzom1b  8835  elfzomelpfzo  8837  peano2fzor  8838  fzoshftral  8844  frec2uzzd  8847  frec2uzuzd  8849  frec2uzltd  8850  frec2uzlt2d  8851  frecuzrdgrrn  8855  frecuzrdgfn  8859  frecuzrdgsuc  8862  fzofig  8869  nn0ennn  8870  iseqfveq2  8885  iseqfeq2  8886  expivallem  8890  expival  8891  expinnval  8892  exp1  8895  expp1  8896  expnegap0  8897  expm1t  8917  expap0  8919  expadd  8931  expsubap  8936  leexp1a  8943  subsq  8991  subsq2  8992  binom2sub  8997  bernneq  9002  bernneq3  9004  expnlbnd  9006  crre  9065  rereb  9071  mulreap  9072  readd  9077  resub  9078  remullem  9079  imadd  9085  imsub  9086  cjadd  9092  ipcnval  9094  cjsub  9100  sqrt0  9193  cbvrald  9242  bdsepnft  9321  bj-om  9371  bj-nnen2lp  9388  strcollnft  9414  sscoll2  9418
  Copyright terms: Public domain W3C validator