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  6504  genprndu  6505  genpdisj  6506  genpassl  6507  genpassu  6508  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  addlocprlemeqgt  6515  nqprloc  6528  addnqpr1lemrl  6537  addnqpr1lemru  6538  addnqpr1lemil  6539  addnqpr1lemiu  6540  appdivnq  6542  prmuloc  6545  mulnqprl  6547  mulnqpru  6548  mullocprlem  6549  distrlem4prl  6558  distrlem4pru  6559  1idprl  6564  1idpru  6565  ltpopr  6567  ltsopr  6568  ltaddpr  6569  ltexprlemupu  6576  ltexprlemdisj  6578  ltexprlemloc  6579  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  addcanprleml  6586  ltaprg  6590  addextpr  6591  recexprlemdisj  6600  recexprlemloc  6601  recexprlem1ssl  6603  recexprlem1ssu  6604  aptiprleml  6609  aptiprlemu  6610  mulcmpblnrlemg  6628  ltsrprg  6635  mulasssrg  6646  distrsrg  6647  lttrsr  6650  ltposr  6651  ltsosr  6652  0idsr  6655  1idsr  6656  ltasrg  6658  recexgt0sr  6661  mulgt0sr  6664  mulextsr1lem  6666  archsr  6668  axmulass  6717  axdistr  6718  ax0id  6722  axcnre  6725  ltxrlt  6842  ltso  6853  muladd11  6903  readdcan  6910  cnegexlem1  6943  cnegexlem3  6945  cnegex  6946  addsubeq4  6983  subeq0  6993  renegcl  7028  mul2neg  7151  submul2  7152  ltleadd  7196  ltaddpos  7202  lt2sub  7210  le2sub  7211  lenegcon2  7217  recexre  7322  apirr  7349  apsym  7350  apneg  7355  apti  7366  recextlem1  7374  recexap  7376  mulap0  7377  divvalap  7395  rec11ap  7428  divdivdivap  7431  divmul24ap  7434  divmuleqap  7435  divadddivap  7445  conjmulap  7447  letrp1  7555  ltdivmul  7583  lerec2  7596  ledivdiv  7597  cju  7654  nn1suc  7674  nn2ge  7687  nnsub  7693  nndiv  7695  halfaddsub  7896  nn0addcl  7953  nn0mulcl  7954  elnn0nn  7960  nn0ge2m1nn  7978  znegcl  8012  zaddcllempos  8018  zaddcllemneg  8020  zaddcl  8021  ztri3or  8024  zltnle  8027  zltp1le  8034  zltlem1  8037  elz2  8048  zdceq  8052  zdclt  8054  zdivadd  8065  gtndiv  8071  prime  8073  zneo  8075  zeo  8079  peano2uz2  8081  uzind  8085  fzind  8089  eluzuzle  8217  uztrn  8225  eluzp1l  8233  peano2uzr  8264  uzaddcl  8265  indstr  8272  indstr2  8282  ublbneg  8284  divfnzn  8292  qmulz  8294  qaddcl  8306  qnegcl  8307  qapne  8310  qreccl  8311  irradd  8315  irrmul  8316  xrltnsym  8444  xrlttr  8446  xrltso  8447  xrlttri3  8448  xrre  8463  xrre2  8464  xrre3  8465  xltnegi  8478  ixxss1  8503  ixxss2  8504  ixxss12  8505  ubioog  8513  iccss2  8543  iccssioo2  8545  iccssico2  8546  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  divelunit  8600  lincmb01cmp  8601  iccf1o  8602  fztri3or  8633  uzsubsubfz  8641  fzsplit2  8644  fzdisj  8646  fzaddel  8652  fzsubel  8653  fzss1  8656  fzss2  8657  fznatpl1  8668  fzdifsuc  8673  fzrev  8676  fzrev2  8677  fzrev2i  8678  fzrev3  8679  elfzm11  8683  uzsplit  8684  fzm1  8692  fzneuz  8693  elfz2nn0  8703  elfz0addOLD  8710  elfz0fzfz0  8713  fz0fzelfz0  8714  uzsubfz0  8716  fz0fzdiffz0  8717  elfzmlbmOLD  8719  elfzmlbp  8720  difelfzle  8722  difelfznle  8723  1fv  8726  fzon  8752  fzoss1  8757  fzouzdisj  8766  fzo1fzo0n0  8769  elfzo0z  8770  fzofzim  8774  fzoaddel2  8779  fzosubel2  8781  eluzgtdifelfzo  8783  elfzodifsumelfzo  8787  zpnn0elfzo1  8794  fzosplitsnm1  8795  elfzom1p1elfzo  8800  ssfzo12bi  8811  ubmelm1fzo  8812  fzofzp1b  8814  elfzom1b  8815  elfzomelpfzo  8817  peano2fzor  8818  fzoshftral  8824  frec2uzzd  8827  frec2uzuzd  8829  frec2uzltd  8830  frec2uzlt2d  8831  frecuzrdgrrn  8835  frecuzrdgfn  8839  frecuzrdgsuc  8842  fzofig  8849  nn0ennn  8850  iseqfveq2  8865  iseqfeq2  8866  expivallem  8870  expival  8871  expinnval  8872  exp1  8875  expp1  8876  expnegap0  8877  expm1t  8897  expap0  8899  expadd  8911  expsubap  8916  leexp1a  8923  subsq  8971  subsq2  8972  binom2sub  8977  bernneq  8982  bernneq3  8984  expnlbnd  8986  crre  9045  rereb  9051  mulreap  9052  readd  9057  resub  9058  remullem  9059  imadd  9065  imsub  9066  cjadd  9072  ipcnval  9074  cjsub  9080  cbvrald  9196  bdsepnft  9275  bj-om  9325  bj-nnen2lp  9342  strcollnft  9368  sscoll2  9372
  Copyright terms: Public domain W3C validator