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  438  ad2antrr  460  ad3antrrr  461  ad2antlr  462  ad2antrl  463  im2anan9  517  bi2bian9  528  jaao  626  ordi  717  con1bidc  756  con1bdc  760  pm5.18dc  765  dfandc  766  pm4.54dc  793  stabtestimpdc  812  ccase2  859  simpl1  893  simpl2  894  simpl3  895  3ad2ant1  911  3ad2ant2  912  simpll1  929  simpll2  930  simpll3  931  simplr1  932  simplr2  933  simplr3  934  simpl1l  941  simpl1r  942  simpl2l  943  simpl2r  944  simpl3l  945  simpl3r  946  simpl11  965  simpl12  966  simpl13  967  simpl21  968  simpl22  969  simpl23  970  simpl31  971  simpl32  972  simpl33  973  xorbin  1256  biassdc  1267  bilukdc  1268  sbequi  1698  nfsbxyt  1797  euan  1934  datisi  1988  fresison  1996  ralbid  2298  rexbid  2299  ralimdv  2362  reubidv  2467  rmobidv  2472  rabbidv  2523  elex22  2542  gencbvex  2573  rspct  2622  ceqsrexbv  2648  elrabf  2669  eueq3dc  2688  reu6  2703  reuind  2717  csbcomg  2846  csbiebt  2859  eldif  2900  sseq1  2939  undif3ss  3171  difrab  3184  disjpr2  3404  diftpsn3  3475  preqr1g  3507  nfopd  3536  eluni  3553  dfnfc2  3568  iuneq12d  3651  iuneq2d  3652  disjeq12d  3724  disjxsn  3732  mpteq12dv  3809  mpteq2dv  3818  trel  3831  csbexgOLD  3855  opexg  3934  opexgOLD  3935  opm  3941  copsexg  3951  euotd  3961  elopab  3965  epelg  3997  sotritrieq  4032  suctr  4104  alxfr  4139  rexxfrd  4141  op1stbg  4156  ordelsuc  4177  onsucelsucr  4179  onsucelsucexmidlem  4194  en2lp  4212  preleq  4213  opthreg  4214  ordsuc  4221  peano5  4244  poinxp  4332  sosng  4336  eqrelrdv2  4362  xpsspw  4373  relopabi  4386  opeliunxp2  4399  relop  4409  opeldmg  4463  xpid11m  4480  riinint  4516  asymref  4633  xpidtr  4638  ssxpbm  4679  ssxp1  4680  ssxp2  4681  xpexr2m  4685  rnpropg  4723  elxp4  4731  elxp5  4732  funeu  4848  funun  4866  fununi  4889  funimaexglem  4904  funfni  4921  fneu  4925  fco  4977  funssxp  4981  feu  4993  fimacnvdisj  4995  f1ss  5018  f1ssr  5019  f1ssres  5020  f1imacnv  5064  foimacnv  5065  fun11iun  5068  f1o00  5082  nffvd  5108  fnbrfvb  5135  fvelrnb  5142  fvelimab  5150  ssimaex  5155  fvopab3g  5166  fvmptssdm  5176  fvmpt2d  5178  fvmptdf  5179  eqfnfv  5186  fndmdif  5193  fndmin  5195  fneqeql2  5197  fvimacnv  5203  ffvelrn  5221  dff3im  5233  dffo3  5235  fmptco  5251  fcompt  5254  fsn2  5258  fprg  5267  fvunsng  5278  fsnunres  5285  resfunexg  5303  fnex  5304  f1ocnvfv1  5338  f1ocnvfv2  5339  foeqcnvco  5351  f1eqcocnv  5352  fliftf  5360  fliftval  5361  isocnv  5372  isocnv2  5373  isores3  5376  isoini  5378  isoini2  5379  isoselem  5380  riota2df  5408  acexmid  5431  oprabid  5457  0neqopab  5469  mpt2eq123dv  5486  cbvmpt2x  5501  eloprabga  5510  ovmpt2dxf  5545  ovmpt2df  5551  ov6g  5557  oprssov  5561  caovord3  5593  caovimo  5613  grprinvlem  5614  grprinvd  5615  f1opw2  5625  suppssfv  5627  suppssov1  5628  fnofval  5640  off  5643  offval2  5645  ofrfval2  5646  ofc12  5650  caofref  5651  caofinvl  5652  caofrss  5654  caoftrn  5655  fnexALT  5659  iunexg  5665  offval3  5680  f1stres  5705  elxp6  5715  elxp7  5716  unielxp  5719  xpopth  5721  op1steq  5724  releldm2  5730  dfoprab4  5737  fmpt2x  5745  1stconst  5761  2ndconst  5762  cnvf1o  5765  f1o2ndf1  5768  mpt2xopoveq  5773  isprmpt2  5776  brtpos2  5784  smores2  5827  iordsmo  5830  smoiso  5835  tfrlem1  5841  tfrlem3a  5843  tfrlem4  5847  tfrlem8  5852  tfrlemisucaccv  5856  tfrlemiubacc  5861  tfrlemi1  5863  tfri3  5871  rdgivallem  5884  rdgon  5889  frecrdg  5904  sucinc2  5937  oav2  5954  oaword1  5961  nnmcl  5971  nndi  5976  nnaordi  5988  nnaword  5991  nnmordi  5996  nnmord  5997  nnaordex  6007  nnawordex  6008  nnm00  6009  ersymb  6027  erref  6033  iserd  6039  erth  6057  erinxp  6087  qliftel  6093  qliftfun  6095  eroveu  6104  eroprf  6106  th3qlem1  6115  ecovass  6122  ecoviass  6123  elni2  6168  mulclpi  6182  addasspig  6184  mulasspig  6186  mulcanpig  6189  ltexpi  6191  ltapig  6192  ltmpig  6193  enqeceq  6212  addcmpblnq  6220  dmaddpqlem  6230  distrnqg  6240  mulidnq  6242  ltsonq  6251  ltexnqq  6260  subhalfnqq  6265  ltbtwnnqq  6266  ltbtwnnq  6267  archnqq  6268  ltrnqg  6271  enq0sym  6281  enq0tr  6283  enq0eceq  6286  nqnq0pi  6287  nqnq0  6290  addcmpblnq0  6292  mulnnnq0  6299  nqpnq0nq  6302  nqnq0a  6303  nqnq0m  6304  nq0m0r  6305  distrnq0  6308  addassnq0  6311  nq02m  6313  preqlu  6320  prubl  6334  prloc  6339  prarloclemlt  6341  prarloclemn  6347  prarloc  6351  prarloc2  6352  genpml  6366  genpmu  6367  genpcdl  6368  genpcuu  6369  genprndl  6370  genprndu  6371  genpassl  6373  genpassu  6374  addlocprlemeq  6382  addlocprlemgt  6383  addlocpr  6385  appdivnq  6401  appdiv0nq  6402  mulnqprl  6406  mulnqpru  6407  mullocprlem  6408  mullocpr  6409  distrlem1prl  6415  distrlem1pru  6416  distrlem4prl  6417  distrlem4pru  6418  ltprordil  6422  1idprl  6423  1idpru  6424  ltpopr  6426  ltsopr  6427  ltaddpr  6428  ltexprlemm  6431  ltexprlemopl  6432  ltexprlemopu  6434  ltexprlemloc  6438  ltexprlemrl  6441  ltexprlemru  6443  addcanprleml  6445  addcanprlemu  6446  addcanprg  6447  ltaprlem  6448  recexprlemell  6450  recexprlemelu  6451  recexprlemm  6452  recexprlemdisj  6458  recexprlempr  6460  recexprlem1ssl  6461  recexprlem1ssu  6462  recexprlemss1l  6463  recexprlemss1u  6464  enreceq  6477  mulcmpblnrlemg  6481  ltsrprg  6488  recexsrlem  6514  addgt0sr  6515  mulgt0sr  6516  ax0id  6566  ltxrlt  6680  ltnsym  6696  ltletr  6699  muladd11  6733  readdcan  6740  cnegexlem1  6773  cnegexlem2  6774  cnegexlem3  6775  cnegex  6776  negeu  6789  npncan2  6824  subneg  6846  negcon1  6849  ltleadd  7026  lt2sub  7040  le2sub  7041  lenegcon1  7046  addge01  7052  leaddle0  7056  mullt0  7058  peano5set  7301  sscoll2  7345
  Copyright terms: Public domain W3C validator