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

Theorem adantr 261
Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
adantr.1 (φψ)
Assertion
Ref Expression
adantr ((φ χ) → ψ)

Proof of Theorem adantr
StepHypRef Expression
1 adantr.1 . . 3 (φψ)
21a1d 22 . 2 (φ → (χψ))
32imp 115 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
This theorem is referenced by:  adantl  262  anim12ii  325  sylan9bb  435  ad2antrr  457  ad2antlr  458  ad2antrl  459  ad3antrrr  461  ad3antlr  462  ad4antr  463  ad4antlr  464  ad5antr  465  ad5antlr  466  ad6antr  467  ad6antlr  468  ad7antr  469  ad7antlr  470  ad8antr  471  ad8antlr  472  ad9antr  473  ad9antlr  474  ad10antr  475  ad10antlr  476  im2anan9  530  bi2bian9  540  jaao  638  ordi  728  con1bidc  767  con1bdc  771  pm5.18dc  776  dfandc  777  pm4.54dc  804  stabtestimpdc  823  ccase2  872  simpl1  906  simpl2  907  simpl3  908  3ad2ant1  924  3ad2ant2  925  simpll1  942  simpll2  943  simpll3  944  simplr1  945  simplr2  946  simplr3  947  simpl1l  954  simpl1r  955  simpl2l  956  simpl2r  957  simpl3l  958  simpl3r  959  simpl11  978  simpl12  979  simpl13  980  simpl21  981  simpl22  982  simpl23  983  simpl31  984  simpl32  985  simpl33  986  xorbin  1272  biassdc  1283  bilukdc  1284  sbequi  1717  nfsbxyt  1816  euan  1953  datisi  2007  fresison  2015  ralbid  2318  rexbid  2319  ralimdv  2382  reubidv  2487  rmobidv  2492  rabbidv  2543  elex22  2563  gencbvex  2594  rspct  2643  ceqsrexbv  2669  elrabf  2690  eueq3dc  2709  reu6  2724  reuind  2738  csbcomg  2867  csbiebt  2880  eldif  2921  sseq1  2960  undif3ss  3192  difrab  3205  disjpr2  3425  diftpsn3  3496  preqr1g  3528  nfopd  3557  eluni  3574  dfnfc2  3589  iuneq12d  3672  iuneq2d  3673  disjeq12d  3745  disjxsn  3753  mpteq12dv  3830  mpteq2dv  3839  trel  3852  csbexga  3876  opexg  3955  opexgOLD  3956  opm  3962  copsexg  3972  euotd  3982  elopab  3986  epelg  4018  sotritrieq  4053  alxfr  4159  rexxfrd  4161  op1stbg  4176  ordelsuc  4197  onsucelsucr  4199  onsucelsucexmidlem  4214  en2lp  4232  preleq  4233  opthreg  4234  ordsuc  4241  peano5  4264  poinxp  4352  sosng  4356  eqrelrdv2  4382  xpsspw  4393  relopabi  4406  opeliunxp2  4419  relop  4429  opeldmg  4483  xpid11m  4500  riinint  4536  asymref  4653  xpidtr  4658  ssxpbm  4699  ssxp1  4700  ssxp2  4701  xpexr2m  4705  rnpropg  4743  elxp4  4751  elxp5  4752  funeu  4869  funun  4887  fununi  4910  funimaexglem  4925  funfni  4942  fneu  4946  fco  4999  funssxp  5003  feu  5015  fimacnvdisj  5017  f1ss  5040  f1ssr  5041  f1ssres  5042  f1imacnv  5086  foimacnv  5087  fun11iun  5090  f1o00  5104  nffvd  5130  fnbrfvb  5157  fvelrnb  5164  fvelimab  5172  ssimaex  5177  fvopab3g  5188  fvmptssdm  5198  fvmpt2d  5200  fvmptdf  5201  eqfnfv  5208  fndmdif  5215  fndmin  5217  fneqeql2  5219  fvimacnv  5225  ffvelrn  5243  dff3im  5255  dffo3  5257  fmptco  5273  fcompt  5276  fsn2  5280  fprg  5289  fvunsng  5300  fsnunres  5307  resfunexg  5325  fnex  5326  f1ocnvfv1  5360  f1ocnvfv2  5361  foeqcnvco  5373  f1eqcocnv  5374  fliftf  5382  fliftval  5383  isocnv  5394  isocnv2  5395  isores3  5398  isoini  5400  isoini2  5401  isoselem  5402  riotaexg  5415  riota2df  5431  acexmid  5454  oprabid  5480  0neqopab  5492  mpt2eq123dv  5509  cbvmpt2x  5524  eloprabga  5533  ovmpt2dxf  5568  ovmpt2df  5574  ov6g  5580  oprssov  5584  caovord3  5616  caovimo  5636  grprinvlem  5637  grprinvd  5638  f1opw2  5648  suppssfv  5650  suppssov1  5651  fnofval  5663  off  5666  offval2  5668  ofrfval2  5669  ofc12  5673  caofref  5674  caofinvl  5675  caofrss  5677  caoftrn  5678  fnexALT  5682  iunexg  5688  offval3  5703  f1stres  5728  elxp6  5738  elxp7  5739  unielxp  5742  xpopth  5744  op1steq  5747  releldm2  5753  dfoprab4  5760  fmpt2x  5768  1stconst  5784  2ndconst  5785  cnvf1o  5788  f1o2ndf1  5791  mpt2xopoveq  5796  isprmpt2  5799  brtpos2  5807  smores2  5850  iordsmo  5853  smoiso  5858  tfrlem1  5864  tfrlem3a  5866  tfrlem4  5870  tfrlem8  5875  tfrlemisucaccv  5880  tfrlemiubacc  5885  tfrlemi1  5887  tfri3  5894  rdgivallem  5908  rdgon  5913  frecrdg  5931  freccl  5932  sucinc2  5965  oav2  5982  oaword1  5989  nnmcl  5999  nndi  6004  nnaordi  6017  nnaword  6020  nnmordi  6025  nnmord  6026  nnaordex  6036  nnawordex  6037  nnm00  6038  ersymb  6056  erref  6062  iserd  6068  erth  6086  erinxp  6116  qliftel  6122  qliftfun  6124  eroveu  6133  eroprf  6135  th3qlem1  6144  ecovass  6151  ecoviass  6152  dom2lem  6188  ssdomg  6194  fundmen  6222  cnven  6224  fndmeng  6225  xpsnen  6231  xpdom2  6241  fopwdom  6246  elni2  6298  mulclpi  6312  addasspig  6314  mulasspig  6316  mulcanpig  6319  ltexpi  6321  ltapig  6322  ltmpig  6323  indpi  6326  enqeceq  6343  addcmpblnq  6351  dmaddpqlem  6361  distrnqg  6371  mulidnq  6373  ltsonq  6382  ltexnqq  6391  subhalfnqq  6397  ltbtwnnqq  6398  ltbtwnnq  6399  archnqq  6400  ltrnqg  6403  enq0sym  6414  enq0tr  6416  enq0eceq  6419  nqnq0pi  6420  nqnq0  6423  addcmpblnq0  6425  mulnnnq0  6432  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  nq0m0r  6438  distrnq0  6441  addassnq0  6444  nq02m  6447  preqlu  6454  prubl  6468  prloc  6473  prarloclemlt  6475  prarloclemn  6481  prarloc  6485  prarloc2  6486  genpml  6500  genpmu  6501  genpcdl  6502  genpcuu  6503  genprndl  6504  genprndu  6505  genpassl  6507  genpassu  6508  addlocprlemeq  6516  addlocprlemgt  6517  addlocpr  6519  addnqpr1lemrl  6537  addnqpr1lemru  6538  addnqpr1lemil  6539  addnqpr1lemiu  6540  appdivnq  6542  appdiv0nq  6543  mulnqprl  6547  mulnqpru  6548  mullocprlem  6549  mullocpr  6550  distrlem1prl  6556  distrlem1pru  6557  distrlem4prl  6558  distrlem4pru  6559  ltprordil  6563  1idprl  6564  1idpru  6565  ltpopr  6567  ltsopr  6568  ltaddpr  6569  ltexprlemm  6572  ltexprlemopl  6573  ltexprlemopu  6575  ltexprlemloc  6579  ltexprlemrl  6582  ltexprlemru  6584  addcanprleml  6586  addcanprlemu  6587  addcanprg  6588  ltaprlem  6589  addextpr  6591  recexprlemell  6592  recexprlemelu  6593  recexprlemm  6594  recexprlemdisj  6600  recexprlempr  6602  recexprlem1ssl  6603  recexprlem1ssu  6604  recexprlemss1l  6605  recexprlemss1u  6606  aptiprleml  6609  aptiprlemu  6610  ltmprr  6612  enreceq  6624  mulcmpblnrlemg  6628  ltsrprg  6635  recexgt0sr  6661  addgt0sr  6663  mulgt0sr  6664  archsr  6668  pitonn  6704  ax0id  6722  ltxrlt  6842  lttri3  6855  ltnsym  6861  ltletr  6864  muladd11  6903  readdcan  6910  cnegexlem1  6943  cnegexlem2  6944  cnegexlem3  6945  cnegex  6946  negeu  6959  npncan2  6994  subneg  7016  negcon1  7019  ltleadd  7196  lt2sub  7210  le2sub  7211  lenegcon1  7216  addge01  7222  leaddle0  7227  mullt0  7230  recexre  7322  reapti  7323  rimul  7329  apreap  7331  ltmul1  7336  apreim  7347  apcotr  7351  mulext1  7356  mulge0  7363  apti  7366  ltleap  7373  recextlem1  7374  recexaplem2  7375  recexap  7376  mulcanapd  7384  divmul13ap  7433  conjmulap  7447  p1le  7556  recgt0  7557  prodgt0gt0  7558  prodgt0  7559  lemul2a  7566  ltmul12a  7567  mulgt1  7570  lemulge12  7574  ltdivmul  7583  ltrec1  7595  ledivdiv  7597  lediv2a  7602  cju  7654  nn1suc  7674  nnmulcl  7676  nn2ge  7687  nnsub  7693  halfaddsub  7896  nnrecl  7915  nn0ge2m1nn  7978  nn0nndivcl  7980  elnn0z  7994  peano2z  8017  zaddcllempos  8018  zaddcllemneg  8020  zaddcl  8021  ztri3or  8024  zletric  8025  zlelttric  8026  zleloe  8028  zrevaddcl  8031  zltp1le  8034  zlem1lt  8036  elz2  8048  zdceq  8052  zdcle  8053  zdclt  8054  nn0n0n1ge2b  8056  nn0lt2  8058  nn0ge0div  8063  zdiv  8064  zdivadd  8065  zdivmul  8066  zextle  8067  msqznn  8074  zneo  8075  zeo  8079  peano5uzti  8082  nn0ind-raph  8091  uztrn  8225  uzss  8229  eluzadd  8237  uzaddcl  8265  indstr  8272  indstr2  8282  nn0ge2m1nnALT  8289  qmulz  8294  qaddcl  8306  qnegcl  8307  qmulcl  8308  qreccl  8311  qrevaddcl  8313  ge0p1rp  8349  rpnegap  8350  ltxr  8425  xrltnsym  8444  xrlttr  8446  xrltso  8447  xrlttri3  8448  xrltletr  8453  xrre2  8464  ge0nemnf  8467  xltnegi  8478  lbioog  8512  iccss2  8543  iccssioo2  8545  iccssico2  8546  iooshf  8551  elioopnf  8566  elioomnf  8567  elicopnf  8568  elxrge0  8577  icoshftf1o  8589  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  lincmb01cmp  8601  iccf1o  8602  elfz5  8612  fztri3or  8633  fznlem  8635  fzn  8636  uzsubsubfz  8641  fzdisj  8646  fzmmmeqm  8651  fzaddel  8652  fzopth  8654  fznatpl1  8668  fzdifsuc  8673  elfz1b  8682  fseq1p1m1  8686  elfzp1b  8689  fzm1  8692  fzneuz  8693  ige2m1fz  8702  elfz0addOLD  8710  elfz0ubfz0  8712  elfz0fzfz0  8713  fz0fzelfz0  8714  fz0fzdiffz0  8717  elfzmlbmOLD  8719  elfzmlbp  8720  difelfzle  8722  difelfznle  8723  nn0disj  8725  1fv  8726  4fvwrd4  8727  fzoss1  8757  fzospliti  8762  fzosplit  8763  fzouzdisj  8766  fzo1fzo0n0  8769  elfzo0z  8770  fzonmapblen  8773  fzofzim  8774  fzoaddel  8778  fzosubel  8780  fzosubel3  8782  eluzgtdifelfzo  8783  elfzodifsumelfzo  8787  elfzom1elp1fzo  8788  zpnn0elfzo1  8794  elfzom1p1elfzo  8800  ssfzo12  8810  ssfzo12bi  8811  ubmelm1fzo  8812  elfzonelfzo  8816  elfzomelpfzo  8817  fzoshftral  8824  frec2uzltd  8830  frec2uzlt2d  8831  frec2uzrand  8832  frec2uzf1od  8833  frec2uzisod  8834  frecuzrdgrrn  8835  frec2uzrdg  8836  frecuzrdgfn  8839  frecuzrdgcl  8840  frecuzrdgsuc  8842  frecfzennn  8844  iseqovex  8859  iseqval  8860  iseqfveq2  8865  iseqfeq2  8866  expivallem  8870  expival  8871  expp1  8876  expn1ap0  8879  expcllem  8880  expcl2lemap  8881  rpexpcl  8888  m1expcl2  8891  expclzaplem  8893  1exp  8898  expap0  8899  expeq0  8900  expnegzap  8903  mulexp  8908  expadd  8911  expaddzaplem  8912  expmul  8914  leexp2r  8922  leexp1a  8923  expubnd  8925  sqgt0ap  8935  subsq  8971  binom2sub  8977  zesq  8980  bernneq  8982  bernneq3  8984  expnbnd  8985  expnlbnd  8986  crre  9045  reim0b  9050  rereb  9051  mulreap  9052  readd  9057  remullem  9059  remul2  9061  imadd  9065  immul2  9068  cjadd  9072  cjexp  9081  cjap  9094  peano5set  9328  sscoll2  9372
  Copyright terms: Public domain W3C validator