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  460  ad2antll  461  im2anan9  515  bi2bian9  525  jaao  623  ordi  713  con1bidc  752  con1bdc  756  dfandc  762  stabtestimpdc  808  dcor  825  annimdc  827  ccase2  855  rnlem  865  simpr1  892  simpr2  893  simpr3  894  3ad2ant3  909  simprl1  931  simprl2  932  simprl3  933  simprr1  934  simprr2  935  simprr3  936  simpr1l  943  simpr1r  944  simpr2l  945  simpr2r  946  simpr3l  947  simpr3r  948  simpr11  970  simpr12  971  simpr13  972  simpr21  973  simpr22  974  simpr23  975  simpr31  976  simpr32  977  simpr33  978  falimd  1238  xorbin  1253  xor2dc  1259  biassdc  1264  dfbi3dc  1266  xordidc  1268  ax11v2  1674  ax11b  1680  equs5or  1684  nfsbxyt  1792  sbcomxyyz  1819  2exeu  1965  dimatis  1990  gencbvex  2568  gencbval  2570  elrab3t  2665  euind  2696  reu6  2698  reuind  2712  sbcan  2773  sbcralt  2802  sbcrext  2803  csbcomg  2841  csbiebt  2854  sbcnestgf  2865  sseq1  2934  ddifnel  3043  elin  3094  undif3ss  3166  uneqdifeqim  3276  disjpr2  3397  diftpsn3  3468  preqr1g  3500  nfopd  3529  unissel  3572  trel  3824  iinexgm  3871  copsex2t  3945  sowlin  4020  ordelon  4058  alxfr  4131  ralxfr  4136  rexxfr  4138  rabxfr  4140  reuhyp  4142  ordelsuc  4169  onsucelsucr  4171  onsucsssucr  4172  ordtriexmidlem  4180  onsucelsucexmidlem  4186  ordsucunielexmid  4188  regexmidlem1  4190  preleq  4205  eunex  4211  ordsuc  4213  nlimsucg  4214  onnmin  4216  tfi  4220  peano2  4233  opeliunxp  4310  posng  4327  sosng  4328  eqrelrdv2  4354  ideqg  4402  opeldmg  4455  relssres  4563  exse2  4614  brcodir  4627  xpidtr  4630  poltletr  4640  ssxpbm  4671  ssxp1  4672  ssxp2  4673  xpexr2m  4677  rnpropg  4715  elxp4  4723  elxp5  4724  dfco2a  4736  iota5  4802  iota2  4808  funssres  4856  funun  4858  fnsng  4861  fununi  4881  funimaexglem  4896  fneu  4917  fco  4969  fco2  4970  funssxp  4973  fssres2  4980  f1orescnv  5055  nffvd  5100  fnsnfv  5145  ssimaex  5147  funfvdm2  5150  dmfco  5154  fvco2  5155  fvmptss2  5160  respreima  5208  rexrn  5217  ralrn  5218  elrnrexdm  5219  ralrnmpt  5222  rexrnmpt  5223  ffvresb  5241  fcompt  5246  xpsng  5251  fprg  5259  fsnunres  5277  resfunexg  5295  funfvima3  5305  rexima  5307  ralima  5308  f1veqaeq  5321  f1ocnvfv1  5330  f1ocnvfv2  5331  fcofo  5337  foeqcnvco  5343  f1eqcocnv  5344  isoresbr  5362  isoini  5370  isoselem  5372  f1oiso  5378  riotabiia  5397  riota2f  5401  riota5f  5404  eloprabga  5502  ovmpt2x  5540  ovmpt2ga  5541  ovg  5550  oprssov  5553  caovcl  5566  caovimo  5605  f1opw2  5617  ofres  5636  resfunexgALT  5648  cofunexg  5649  iunexg  5657  offval3  5672  f2ndres  5698  elxp6  5707  releldm2  5722  oprabco  5749  1stconst  5753  2ndconst  5754  cnvf1o  5757  fo2ndf  5759  f1o2ndf1  5760  poxp  5763  mpt2xopoveq  5765  sprmpt2  5767  isprmpt2  5768  reldmtpos  5778  dftpos4  5788  tposf2  5793  iunon  5809  iordsmo  5822  tfrlem1  5833  tfrlemisucaccv  5848  tfrlemi1  5855  tfrexlem  5858  tfri3  5863  rdgivallem  5876  rdgon  5881  frec0g  5890  oasuc  5947  omsuc  5954  nnaass  5967  nndi  5968  nnsucelsuc  5973  nntri1  5977  nnaordi  5980  nnaword  5983  nnmord  5989  nnm00  6001  swoer  6033  eqer  6037  0er  6039  relelec  6045  ectocl  6072  iinerm  6077  eroveu  6096  ecopovtrn  6102  ecopover  6103  ecopovsymg  6104  ecopovtrng  6105  ecopoverg  6106  th3qlem1  6107  ecovass  6114  ecoviass  6115  ecovdi  6116  ecovidi  6117  ltpiord  6165  ltsopi  6166  mulclpi  6174  addasspig  6176  mulasspig  6178  distrpig  6179  addnidpig  6182  ltapig  6184  ltmpig  6185  nnppipi  6188  enqdc1  6207  addcmpblnq  6212  mulcmpblnq  6213  ordpipqqs  6219  addassnqg  6227  mulcanenq  6230  distrnqg  6232  mulidnq  6234  recmulnqg  6236  ltsonq  6243  ltanqg  6245  ltmnqg  6246  ltaddnq  6251  ltexnqq  6252  halfnqq  6253  ltbtwnnqq  6258  archnqq  6260  prarloclemarch  6261  prarloclemarch2  6262  ltrnqg  6263  enq0tr  6275  enq0er  6276  nqnq0  6282  addcmpblnq0  6284  mulcmpblnq0  6285  mulcanenq0ec  6286  nnnq0lem1  6287  mulnnnq0  6291  nqnq0a  6295  nqnq0m  6296  nq0m0r  6297  nq0a0  6298  distrnq0  6300  addassnq0  6303  nq02m  6305  prcdnql  6324  prcunqu  6325  prubl  6326  prloc  6331  prarloclemlt  6333  prarloclemlo  6334  prarloc  6343  genplt2i  6350  genprndl  6362  genprndu  6363  genpdisj  6364  genpassl  6365  genpassu  6366  addnqprllem  6368  addnqprulem  6369  addnqprl  6370  addnqpru  6371  addlocprlemeqgt  6373  nqprloc  6386  appdivnq  6393  prmuloc  6396  mulnqprl  6398  mulnqpru  6399  mullocprlem  6400  distrlem4prl  6409  distrlem4pru  6410  1idprl  6415  1idpru  6416  ltpopr  6418  ltsopr  6419  ltaddpr  6420  ltexprlemupu  6427  ltexprlemdisj  6429  ltexprlemloc  6430  ltexprlemfl  6432  ltexprlemrl  6433  ltexprlemfu  6434  ltexprlemru  6435  addcanprleml  6437  ltaprg  6441  addextpr  6442  recexprlemdisj  6451  recexprlemloc  6452  recexprlem1ssl  6454  recexprlem1ssu  6455  aptiprleml  6460  aptiprlemu  6461  mulcmpblnrlemg  6478  ltsrprg  6485  mulasssrg  6496  distrsrg  6497  lttrsr  6500  ltposr  6501  ltsosr  6502  0idsr  6505  1idsr  6506  ltasrg  6508  recexgt0sr  6511  mulgt0sr  6514  mulextsr1lem  6516  axmulass  6562  axdistr  6563  ax0id  6567  axcnre  6570  ltxrlt  6685  ltso  6696  muladd11  6746  readdcan  6753  cnegexlem1  6786  cnegexlem3  6788  cnegex  6789  addsubeq4  6826  subeq0  6836  renegcl  6871  mul2neg  6994  submul2  6995  ltleadd  7039  ltaddpos  7045  lt2sub  7053  le2sub  7054  lenegcon2  7060  recexre  7165  apirr  7192  apsym  7193  apneg  7198  apti  7209  recextlem1  7217  recexap  7219  mulap0  7220  divvalap  7238  rec11ap  7271  divdivdivap  7274  divmul24ap  7277  divmuleqap  7278  divadddivap  7288  conjmulap  7290  letrp1  7397  ltdivmul  7425  lerec2  7438  ledivdiv  7439  cju  7496  nn1suc  7516  nn2ge  7529  nnsub  7535  nndiv  7537  halfaddsub  7737  nn0addcl  7791  nn0mulcl  7792  elnn0nn  7798  nn0ge2m1nn  7816  znegcl  7849  zaddcllempos  7855  zaddcllemneg  7857  zaddcl  7858  ztri3or  7861  zltnle  7862  zltp1le  7868  zltlem1  7871  zdceq  7883  zdivadd  7893  gtndiv  7899  prime  7901  zneo  7903  zeo  7907  peano2uz2  7909  uzind  7913  fzind  7917  divfnzn  8038  qmulz  8040  qaddcl  8052  qnegcl  8053  qapne  8056  qreccl  8057  irradd  8061  irrmul  8062  cbvrald  8192  bdsepnft  8271  bj-om  8321  bj-nnen2lp  8338  strcollnft  8364  sscoll2  8368
  Copyright terms: Public domain W3C validator