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  ad3antrrr  458  ad2antlr  459  ad2antrl  460  im2anan9  515  bi2bian9  525  jaao  623  ordi  713  con1bidc  752  con1bdc  756  pm5.18dc  761  dfandc  762  pm4.54dc  789  stabtestimpdc  808  ccase2  855  simpl1  889  simpl2  890  simpl3  891  3ad2ant1  907  3ad2ant2  908  simpll1  925  simpll2  926  simpll3  927  simplr1  928  simplr2  929  simplr3  930  simpl1l  937  simpl1r  938  simpl2l  939  simpl2r  940  simpl3l  941  simpl3r  942  simpl11  961  simpl12  962  simpl13  963  simpl21  964  simpl22  965  simpl23  966  simpl31  967  simpl32  968  simpl33  969  xorbin  1253  biassdc  1264  bilukdc  1265  sbequi  1693  nfsbxyt  1792  euan  1929  datisi  1983  fresison  1991  ralbid  2293  rexbid  2294  ralimdv  2357  reubidv  2462  rmobidv  2467  rabbidv  2518  elex22  2537  gencbvex  2568  rspct  2617  ceqsrexbv  2643  elrabf  2664  eueq3dc  2683  reu6  2698  reuind  2712  csbcomg  2841  csbiebt  2854  eldif  2895  sseq1  2934  undif3ss  3166  difrab  3179  disjpr2  3397  diftpsn3  3468  preqr1g  3500  nfopd  3529  eluni  3546  dfnfc2  3561  iuneq12d  3644  iuneq2d  3645  disjeq12d  3717  disjxsn  3725  mpteq12dv  3802  mpteq2dv  3811  trel  3824  csbexga  3848  opexg  3927  opexgOLD  3928  opm  3934  copsexg  3944  euotd  3954  elopab  3958  epelg  3990  sotritrieq  4025  alxfr  4131  rexxfrd  4133  op1stbg  4148  ordelsuc  4169  onsucelsucr  4171  onsucelsucexmidlem  4186  en2lp  4204  preleq  4205  opthreg  4206  ordsuc  4213  peano5  4236  poinxp  4324  sosng  4328  eqrelrdv2  4354  xpsspw  4365  relopabi  4378  opeliunxp2  4391  relop  4401  opeldmg  4455  xpid11m  4472  riinint  4508  asymref  4625  xpidtr  4630  ssxpbm  4671  ssxp1  4672  ssxp2  4673  xpexr2m  4677  rnpropg  4715  elxp4  4723  elxp5  4724  funeu  4840  funun  4858  fununi  4881  funimaexglem  4896  funfni  4913  fneu  4917  fco  4969  funssxp  4973  feu  4985  fimacnvdisj  4987  f1ss  5010  f1ssr  5011  f1ssres  5012  f1imacnv  5056  foimacnv  5057  fun11iun  5060  f1o00  5074  nffvd  5100  fnbrfvb  5127  fvelrnb  5134  fvelimab  5142  ssimaex  5147  fvopab3g  5158  fvmptssdm  5168  fvmpt2d  5170  fvmptdf  5171  eqfnfv  5178  fndmdif  5185  fndmin  5187  fneqeql2  5189  fvimacnv  5195  ffvelrn  5213  dff3im  5225  dffo3  5227  fmptco  5243  fcompt  5246  fsn2  5250  fprg  5259  fvunsng  5270  fsnunres  5277  resfunexg  5295  fnex  5296  f1ocnvfv1  5330  f1ocnvfv2  5331  foeqcnvco  5343  f1eqcocnv  5344  fliftf  5352  fliftval  5353  isocnv  5364  isocnv2  5365  isores3  5368  isoini  5370  isoini2  5371  isoselem  5372  riota2df  5400  acexmid  5423  oprabid  5449  0neqopab  5461  mpt2eq123dv  5478  cbvmpt2x  5493  eloprabga  5502  ovmpt2dxf  5537  ovmpt2df  5543  ov6g  5549  oprssov  5553  caovord3  5585  caovimo  5605  grprinvlem  5606  grprinvd  5607  f1opw2  5617  suppssfv  5619  suppssov1  5620  fnofval  5632  off  5635  offval2  5637  ofrfval2  5638  ofc12  5642  caofref  5643  caofinvl  5644  caofrss  5646  caoftrn  5647  fnexALT  5651  iunexg  5657  offval3  5672  f1stres  5697  elxp6  5707  elxp7  5708  unielxp  5711  xpopth  5713  op1steq  5716  releldm2  5722  dfoprab4  5729  fmpt2x  5737  1stconst  5753  2ndconst  5754  cnvf1o  5757  f1o2ndf1  5760  mpt2xopoveq  5765  isprmpt2  5768  brtpos2  5776  smores2  5819  iordsmo  5822  smoiso  5827  tfrlem1  5833  tfrlem3a  5835  tfrlem4  5839  tfrlem8  5844  tfrlemisucaccv  5848  tfrlemiubacc  5853  tfrlemi1  5855  tfri3  5863  rdgivallem  5876  rdgon  5881  frecrdg  5896  sucinc2  5929  oav2  5946  oaword1  5953  nnmcl  5963  nndi  5968  nnaordi  5980  nnaword  5983  nnmordi  5988  nnmord  5989  nnaordex  5999  nnawordex  6000  nnm00  6001  ersymb  6019  erref  6025  iserd  6031  erth  6049  erinxp  6079  qliftel  6085  qliftfun  6087  eroveu  6096  eroprf  6098  th3qlem1  6107  ecovass  6114  ecoviass  6115  elni2  6160  mulclpi  6174  addasspig  6176  mulasspig  6178  mulcanpig  6181  ltexpi  6183  ltapig  6184  ltmpig  6185  enqeceq  6204  addcmpblnq  6212  dmaddpqlem  6222  distrnqg  6232  mulidnq  6234  ltsonq  6243  ltexnqq  6252  subhalfnqq  6257  ltbtwnnqq  6258  ltbtwnnq  6259  archnqq  6260  ltrnqg  6263  enq0sym  6273  enq0tr  6275  enq0eceq  6278  nqnq0pi  6279  nqnq0  6282  addcmpblnq0  6284  mulnnnq0  6291  nqpnq0nq  6294  nqnq0a  6295  nqnq0m  6296  nq0m0r  6297  distrnq0  6300  addassnq0  6303  nq02m  6305  preqlu  6312  prubl  6326  prloc  6331  prarloclemlt  6333  prarloclemn  6339  prarloc  6343  prarloc2  6344  genpml  6358  genpmu  6359  genpcdl  6360  genpcuu  6361  genprndl  6362  genprndu  6363  genpassl  6365  genpassu  6366  addlocprlemeq  6374  addlocprlemgt  6375  addlocpr  6377  appdivnq  6393  appdiv0nq  6394  mulnqprl  6398  mulnqpru  6399  mullocprlem  6400  mullocpr  6401  distrlem1prl  6407  distrlem1pru  6408  distrlem4prl  6409  distrlem4pru  6410  ltprordil  6414  1idprl  6415  1idpru  6416  ltpopr  6418  ltsopr  6419  ltaddpr  6420  ltexprlemm  6423  ltexprlemopl  6424  ltexprlemopu  6426  ltexprlemloc  6430  ltexprlemrl  6433  ltexprlemru  6435  addcanprleml  6437  addcanprlemu  6438  addcanprg  6439  ltaprlem  6440  addextpr  6442  recexprlemell  6443  recexprlemelu  6444  recexprlemm  6445  recexprlemdisj  6451  recexprlempr  6453  recexprlem1ssl  6454  recexprlem1ssu  6455  recexprlemss1l  6456  recexprlemss1u  6457  aptiprleml  6460  aptiprlemu  6461  ltmprr  6463  enreceq  6474  mulcmpblnrlemg  6478  ltsrprg  6485  recexgt0sr  6511  addgt0sr  6513  mulgt0sr  6514  ax0id  6567  ltxrlt  6685  lttri3  6698  ltnsym  6704  ltletr  6707  muladd11  6746  readdcan  6753  cnegexlem1  6786  cnegexlem2  6787  cnegexlem3  6788  cnegex  6789  negeu  6802  npncan2  6837  subneg  6859  negcon1  6862  ltleadd  7039  lt2sub  7053  le2sub  7054  lenegcon1  7059  addge01  7065  leaddle0  7070  mullt0  7073  recexre  7165  reapti  7166  rimul  7172  apreap  7174  ltmul1  7179  apreim  7190  apcotr  7194  mulext1  7199  mulge0  7206  apti  7209  ltleap  7216  recextlem1  7217  recexaplem2  7218  recexap  7219  mulcanapd  7227  divmul13ap  7276  conjmulap  7290  p1le  7398  recgt0  7399  prodgt0gt0  7400  prodgt0  7401  lemul2a  7408  ltmul12a  7409  mulgt1  7412  lemulge12  7416  ltdivmul  7425  ltrec1  7437  ledivdiv  7439  lediv2a  7444  cju  7496  nn1suc  7516  nnmulcl  7518  nn2ge  7529  nnsub  7535  halfaddsub  7737  nn0ge2m1nn  7816  nn0nndivcl  7818  elnn0z  7832  peano2z  7854  zaddcllempos  7855  zaddcllemneg  7857  zaddcl  7858  ztri3or  7861  zrevaddcl  7865  zltp1le  7868  zlem1lt  7870  zdceq  7883  nn0lt2  7886  nn0ge0div  7891  zdiv  7892  zdivadd  7893  zdivmul  7894  zextle  7895  msqznn  7902  zneo  7903  zeo  7907  peano5uzti  7910  nn0ind-raph  7919  qmulz  8040  qaddcl  8052  qnegcl  8053  qmulcl  8054  qreccl  8057  qrevaddcl  8059  ge0p1rp  8094  rpnegap  8095  peano5set  8324  sscoll2  8368
  Copyright terms: Public domain W3C validator