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

Theorem adantr 265
Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
adantr.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
adantr  |-  ( (
ph  /\  ch )  ->  ps )

Proof of Theorem adantr
StepHypRef Expression
1 adantr.1 . . 3  |-  ( ph  ->  ps )
21a1d 22 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 119 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem is referenced by:  adantl  266  anim12ii  329  sylan9bb  443  ad2antrr  465  ad2antlr  466  ad2antrl  467  ad3antrrr  469  ad3antlr  470  ad4antr  471  ad4antlr  472  ad5antr  473  ad5antlr  474  ad6antr  475  ad6antlr  476  ad7antr  477  ad7antlr  478  ad8antr  479  ad8antlr  480  ad9antr  481  ad9antlr  482  ad10antr  483  ad10antlr  484  im2anan9  540  bi2bian9  550  jaao  649  ordi  740  con1bidc  779  con1bdc  783  pm5.18dc  788  dfandc  789  pm4.54dc  816  stabtestimpdc  835  ccase2  884  simpl1  918  simpl2  919  simpl3  920  3ad2ant1  936  3ad2ant2  937  simpll1  954  simpll2  955  simpll3  956  simplr1  957  simplr2  958  simplr3  959  simpl1l  966  simpl1r  967  simpl2l  968  simpl2r  969  simpl3l  970  simpl3r  971  simpl11  990  simpl12  991  simpl13  992  simpl21  993  simpl22  994  simpl23  995  simpl31  996  simpl32  997  simpl33  998  xorbin  1291  biassdc  1302  bilukdc  1303  sbequi  1736  nfsbxyt  1835  euan  1972  datisi  2026  fresison  2034  ralbid  2341  rexbid  2342  ralimdv  2405  reubidv  2510  rmobidv  2515  rabbidv  2566  elex22  2586  gencbvex  2617  rspct  2666  ceqsrexbv  2697  elrabf  2718  eueq3dc  2737  reu6  2752  reuind  2766  csbcomg  2900  csbiebt  2913  eldif  2954  sseq1  2993  undif3ss  3225  difrab  3238  ifcldcd  3385  disjpr2  3461  diftpsn3  3532  preqr1g  3564  nfopd  3593  eluni  3610  dfnfc2  3625  iuneq12d  3708  iuneq2d  3709  disjeq12d  3781  disjxsn  3789  mpteq12dv  3866  mpteq2dv  3875  trel  3888  csbexga  3912  opexg  3991  opexgOLD  3992  opm  3998  copsexg  4008  euotd  4018  elopab  4022  epelg  4054  sotritrieq  4089  frirrg  4114  wepo  4123  alxfr  4220  rexxfrd  4222  op1stbg  4237  ordelsuc  4258  onsucelsucr  4261  onintonm  4270  onsucelsucexmidlem  4281  reg2exmidlema  4286  en2lp  4305  preleq  4306  opthreg  4307  ordsuc  4314  onsucuni2  4315  onintexmid  4324  wetriext  4328  reg3exmidlemwe  4330  peano5  4348  poinxp  4436  sosng  4440  eqrelrdv2  4466  xpsspw  4477  relopabi  4490  opeliunxp2  4503  relop  4513  opeldmg  4567  xpid11m  4584  riinint  4620  asymref  4737  xpidtr  4742  ssxpbm  4783  ssxp1  4784  ssxp2  4785  xpexr2m  4789  rnpropg  4827  elxp4  4835  elxp5  4836  funeu  4953  funun  4971  fununi  4994  funimaexglem  5009  funfni  5026  fneu  5030  fco  5083  funssxp  5087  feu  5099  fimacnvdisj  5101  f1ss  5124  f1ssr  5125  f1ssres  5126  f1imacnv  5170  foimacnv  5171  fun11iun  5174  f1o00  5188  nffvd  5214  fnbrfvb  5241  fvelrnb  5248  fvelimab  5256  ssimaex  5261  fvopab3g  5272  fvmptssdm  5282  fvmpt2d  5284  fvmptdf  5285  eqfnfv  5292  fndmdif  5299  fndmin  5301  fneqeql2  5303  fvimacnv  5309  ffvelrn  5327  dff3im  5339  dffo3  5341  fmptco  5357  fcompt  5360  fsn2  5364  fprg  5373  fvunsng  5384  fsnunres  5391  resfunexg  5409  fnex  5410  f1ocnvfv1  5444  f1ocnvfv2  5445  foeqcnvco  5457  f1eqcocnv  5458  fliftf  5466  fliftval  5467  isocnv  5478  isocnv2  5479  isores3  5482  isoini  5484  isoini2  5485  isoselem  5486  riotaexg  5499  riota2df  5515  acexmid  5538  oprabid  5564  0neqopab  5577  mpt2eq123dv  5594  cbvmpt2x  5609  eloprabga  5618  ovmpt2dxf  5653  ovmpt2df  5659  ov6g  5665  oprssov  5669  caovord3  5701  caovimo  5721  grprinvlem  5722  grprinvd  5723  f1opw2  5733  suppssfv  5735  suppssov1  5736  fnofval  5748  off  5751  offval2  5753  ofrfval2  5754  ofc12  5758  caofref  5759  caofinvl  5760  caofrss  5762  caoftrn  5763  fnexALT  5767  iunexg  5773  offval3  5788  f1stres  5813  elxp6  5823  elxp7  5824  unielxp  5827  xpopth  5829  op1steq  5832  releldm2  5838  dfoprab4  5845  fmpt2x  5853  1stconst  5869  2ndconst  5870  cnvf1o  5873  f1o2ndf1  5876  f1od2  5883  mpt2xopoveq  5885  isprmpt2  5888  brtpos2  5896  smores2  5939  iordsmo  5942  smoiso  5947  tfrlem1  5953  tfrlem3a  5955  tfrlem4  5959  tfrlem8  5964  tfrlemisucaccv  5969  tfrlemiubacc  5974  tfrlemi1  5976  tfri3  5983  rdgivallem  5998  rdgon  6003  frecrdg  6022  freccl  6023  sucinc2  6056  oav2  6073  oaword1  6080  nnmcl  6090  nndi  6095  nntri2or2  6106  nnaordi  6111  nnaword  6114  nnmordi  6119  nnmord  6120  nnaordex  6130  nnawordex  6131  nnm00  6132  ersymb  6150  erref  6156  iserd  6162  erth  6180  erinxp  6210  qliftel  6216  qliftfun  6218  eroveu  6227  eroprf  6229  th3qlem1  6238  ecovass  6245  ecoviass  6246  dom2lem  6282  ssdomg  6288  fundmen  6316  cnven  6318  fndmeng  6319  xpsnen  6325  xpdom2  6335  fopwdom  6340  phplem2  6346  nneneq  6350  nndomo  6356  phpm  6357  fidifsnen  6361  dif1en  6367  php5fin  6369  fin0  6372  fin0or  6373  findcard2  6376  findcard2s  6377  findcard2d  6378  findcard2sd  6379  diffisn  6380  diffifi  6381  fientri3  6383  onunsnss  6385  snon0  6386  supsnti  6408  supisolem  6411  ordiso2  6414  ordiso  6415  carden2bex  6426  elni2  6469  mulclpi  6483  addasspig  6485  mulasspig  6487  mulcanpig  6490  ltexpi  6492  ltapig  6493  ltmpig  6494  indpi  6497  enqeceq  6514  addcmpblnq  6522  dmaddpqlem  6532  distrnqg  6542  mulidnq  6544  ltsonq  6553  ltexnqq  6563  subhalfnqq  6569  ltbtwnnqq  6570  ltbtwnnq  6571  archnqq  6572  ltrnqg  6575  enq0sym  6587  enq0tr  6589  enq0eceq  6592  nqnq0pi  6593  nqnq0  6596  addcmpblnq0  6598  mulnnnq0  6605  nqpnq0nq  6608  nqnq0a  6609  nqnq0m  6610  nq0m0r  6611  distrnq0  6614  addassnq0  6617  nq02m  6620  preqlu  6627  prubl  6641  prloc  6646  prarloclemlt  6648  prarloclemn  6654  prarloc  6658  prarloc2  6659  genpml  6672  genpmu  6673  genpcdl  6674  genpcuu  6675  genprndl  6676  genprndu  6677  genpassl  6679  genpassu  6680  addlocprlemeq  6688  addlocprlemgt  6689  addlocpr  6691  nqprl  6706  nqpru  6707  addnqprlemrl  6712  addnqprlemru  6713  addnqprlemfl  6714  addnqprlemfu  6715  appdivnq  6718  appdiv0nq  6719  mulnqprl  6723  mulnqpru  6724  mullocprlem  6725  mullocpr  6726  mulnqprlemrl  6728  mulnqprlemru  6729  mulnqprlemfl  6730  mulnqprlemfu  6731  distrlem1prl  6737  distrlem1pru  6738  distrlem4prl  6739  distrlem4pru  6740  ltprordil  6744  1idprl  6745  1idpru  6746  ltpopr  6750  ltsopr  6751  ltaddpr  6752  ltexprlemm  6755  ltexprlemopl  6756  ltexprlemopu  6758  ltexprlemloc  6762  ltexprlemrl  6765  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  addcanprg  6771  ltaprlem  6773  prplnqu  6775  addextpr  6776  recexprlemell  6777  recexprlemelu  6778  recexprlemm  6779  recexprlemdisj  6785  recexprlempr  6787  recexprlem1ssl  6788  recexprlem1ssu  6789  recexprlemss1l  6790  recexprlemss1u  6791  aptiprleml  6794  aptiprlemu  6795  ltmprr  6797  cauappcvgprlemopu  6803  cauappcvgprlemdisj  6806  cauappcvgprlemloc  6807  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  cauappcvgprlem1  6814  cauappcvgprlem2  6815  cauappcvgprlemlim  6816  archrecnq  6818  caucvgprlemnkj  6821  caucvgprlemnbj  6822  caucvgprlemopu  6826  caucvgprlemdisj  6829  caucvgprlemloc  6830  caucvgprlemladdfu  6832  caucvgprlem2  6835  caucvgprprlemval  6843  caucvgprprlemnkltj  6844  caucvgprprlemnkeqj  6845  caucvgprprlemnjltk  6846  caucvgprprlemnbj  6848  caucvgprprlemmu  6850  caucvgprprlemopl  6852  caucvgprprlemopu  6854  caucvgprprlemdisj  6857  caucvgprprlemloc  6858  caucvgprprlemexbt  6861  caucvgprprlemexb  6862  caucvgprprlemaddq  6863  caucvgprprlem2  6865  enreceq  6878  mulcmpblnrlemg  6882  ltsrprg  6889  recexgt0sr  6915  addgt0sr  6917  mulgt0sr  6919  archsr  6923  prsrriota  6929  caucvgsrlemcau  6934  caucvgsrlemgt1  6936  caucvgsrlemoffval  6937  caucvgsrlemofff  6938  caucvgsrlemoffcau  6939  caucvgsrlemoffgt1  6940  caucvgsrlemoffres  6941  caucvgsr  6943  pitonn  6981  ltrennb  6987  ax0id  7009  rereceu  7020  recriota  7021  axcaucvglemval  7028  axcaucvglemcau  7029  axcaucvglemres  7030  ltxrlt  7143  lttri3  7156  ltnsym  7162  ltletr  7165  muladd11  7206  readdcan  7213  cnegexlem1  7248  cnegexlem2  7249  cnegexlem3  7250  cnegex  7251  negeu  7264  npncan2  7300  subneg  7322  negcon1  7325  addid0  7442  lelttrdi  7494  ltleadd  7514  lt2sub  7528  le2sub  7529  lenegcon1  7534  addge01  7540  leaddle0  7545  mullt0  7548  recexre  7642  reapti  7643  rimul  7649  apreap  7651  ltmul1  7656  apreim  7667  apcotr  7671  mulext1  7676  mulge0  7683  apti  7686  ltleap  7694  recextlem1  7705  recexaplem2  7706  recexap  7707  mulcanapd  7715  divmul13ap  7765  conjmulap  7779  p1le  7889  recgt0  7890  prodgt0gt0  7891  prodgt0  7892  lemul2a  7899  ltmul12a  7900  mulgt1  7903  lemulge12  7907  ltdivmul  7916  ltrec1  7928  ledivdiv  7930  lediv2a  7935  cju  7988  nn1suc  8008  nnmulcl  8010  nn2ge  8021  nnsub  8027  halfaddsub  8215  div4p1lem1div2  8234  nnrecl  8236  nn0ge2m1nn  8298  nn0nndivcl  8300  elnn0z  8314  peano2z  8337  zaddcllempos  8338  zaddcllemneg  8340  zaddcl  8341  ztri3or  8344  zletric  8345  zlelttric  8346  zleloe  8348  zrevaddcl  8351  zltp1le  8355  zlem1lt  8357  elz2  8369  zdceq  8373  zdcle  8374  zdclt  8375  nn0n0n1ge2b  8377  nn0lt2  8379  nn0ge0div  8384  zdiv  8385  zdivadd  8386  zdivmul  8387  zextle  8388  msqznn  8396  zneo  8397  zeo  8401  peano5uzti  8404  nn0ind-raph  8413  uztrn  8584  uzss  8588  eluzadd  8596  uzaddcl  8624  indstr  8631  indstr2  8642  nn0ge2m1nnALT  8649  qmulz  8654  qaddcl  8666  qnegcl  8667  qmulcl  8668  qreccl  8673  qrevaddcl  8675  ge0p1rp  8711  rpnegap  8712  divlt1lt  8747  divle1le  8748  ledivge1le  8749  nnledivrp  8783  nn0ledivnn  8784  ltxr  8795  xrltnsym  8814  xrlttr  8816  xrltso  8817  xrlttri3  8818  xrltletr  8823  xrre2  8834  ge0nemnf  8837  xltnegi  8848  lbioog  8882  iccss2  8913  iccssioo2  8915  iccssico2  8916  iooshf  8921  elioopnf  8936  elioomnf  8937  elicopnf  8938  elxrge0  8947  icoshftf1o  8959  iccshftr  8962  iccshftl  8964  iccdil  8966  icccntr  8968  lincmb01cmp  8971  iccf1o  8972  zltaddlt1le  8974  elfz5  8983  fztri3or  9004  fznlem  9006  fzn  9007  uzsubsubfz  9012  fzdisj  9017  fzmmmeqm  9022  fzaddel  9023  fzopth  9025  fznatpl1  9039  fzdifsuc  9044  elfz1b  9053  fseq1p1m1  9057  elfzp1b  9060  fzm1  9063  fzneuz  9064  ige2m1fz  9073  elfz0addOLD  9081  elfz0ubfz0  9083  elfz0fzfz0  9084  fz0fzelfz0  9085  fz0fzdiffz0  9088  elfzmlbmOLD  9090  elfzmlbp  9091  difelfzle  9093  difelfznle  9094  nn0disj  9096  1fv  9097  4fvwrd4  9098  fzoss1  9128  fzospliti  9133  fzosplit  9134  fzouzdisj  9137  fzo1fzo0n0  9140  elfzo0z  9141  fzonmapblen  9144  fzofzim  9145  fzoaddel  9149  fzosubel  9151  fzosubel3  9153  eluzgtdifelfzo  9154  elfzodifsumelfzo  9158  elfzom1elp1fzo  9159  zpnn0elfzo1  9165  elfzom1p1elfzo  9171  ssfzo12  9181  ssfzo12bi  9182  ubmelm1fzo  9183  elfzonelfzo  9187  elfzomelpfzo  9188  fzoshftral  9195  fvinim0ffz  9197  subfzo0  9198  qletric  9200  qlelttric  9201  qdceq  9203  qbtwnre  9212  qbtwnxr  9213  qavgle  9214  ico0  9217  ioc0  9218  flqge  9231  flqltnz  9236  flqbi  9239  flqge0nn0  9242  flqge1nn  9243  flqaddz  9246  btwnzge0  9249  flltdivnn0lt  9253  fldiv4p1lem1div2  9254  flqeqceilz  9267  intfracq  9269  flqdiv  9270  zmod1congr  9290  zmodcl  9293  zmodfz  9295  modqid0  9299  zmodid2  9301  modqmuladdnn0  9317  modqm1p1mod0  9324  q2txmodxeq0  9333  q2submod  9334  modifeq2int  9335  modaddmodup  9336  modaddmodlo  9337  modqaddmulmod  9340  modqsubdir  9342  modfzo0difsn  9344  modsumfzodifsn  9345  addmodlteq  9347  frec2uzltd  9352  frec2uzlt2d  9353  frec2uzrand  9354  frec2uzf1od  9355  frec2uzisod  9356  frecuzrdgrrn  9357  frec2uzrdg  9358  frecuzrdgfn  9361  frecuzrdgcl  9362  frecuzrdgsuc  9364  frecfzennn  9366  iseqovex  9382  iseqval  9383  iseqf  9387  iseqss  9389  iseqfveq2  9391  iseqfeq2  9392  iseqfeq  9394  iseqshft2  9395  monoord  9398  monoord2  9399  isermono  9400  iseqsplit  9401  iseqcaopr3  9403  iseqcaopr2  9404  iseqid3  9408  iseqid3s  9409  iseqid  9410  iseqhomo  9411  iseqz  9412  iseqdistr  9413  expivallem  9420  expival  9421  expp1  9426  expn1ap0  9429  expcllem  9430  expcl2lemap  9431  rpexpcl  9438  m1expcl2  9441  expclzaplem  9443  1exp  9448  expap0  9449  expeq0  9450  expnegzap  9453  mulexp  9458  expadd  9461  expaddzaplem  9462  expmul  9464  leexp2r  9473  leexp1a  9474  expubnd  9476  sqgt0ap  9487  subsq  9524  binom2sub  9530  zesq  9534  bernneq  9536  bernneq3  9538  expnbnd  9539  expnlbnd  9540  sqoddm1div8  9568  nn0opthlem2d  9588  nn0opthd  9589  facnn2  9601  facdiv  9605  facwordi  9607  faclbnd  9608  faclbnd3  9610  faclbnd6  9611  facubnd  9612  facavg  9613  bcval4  9619  bccmpl  9621  ibcval5  9630  bcpasc  9633  shftlem  9644  shftuz  9645  shftfvalg  9646  shftfval  9649  shftfn  9652  shftval3  9655  shftcan2  9663  crre  9684  reim0b  9689  rereb  9690  mulreap  9691  readd  9696  remullem  9698  remul2  9700  imadd  9704  immul2  9707  cjadd  9711  cjexp  9720  cjap  9733  caucvgre  9807  cvg1nlemf  9809  cvg1nlemres  9811  cvg1n  9812  rexanuz2  9817  recvguniq  9821  resqrexlem1arp  9831  resqrexlemp1rp  9832  resqrexlemfp1  9835  resqrexlemover  9836  resqrexlemdec  9837  resqrexlemlo  9839  resqrexlemcalc1  9840  resqrexlemcalc2  9841  resqrexlemcalc3  9842  resqrexlemnm  9844  resqrexlemcvg  9845  resqrexlemgt0  9846  resqrexlemoverl  9847  resqrexlemglsq  9848  resqrexlemga  9849  resqrexlemex  9851  rersqrtthlem  9856  sqrtmul  9861  sqrtsq2  9869  absrpclap  9887  absnid  9899  absexp  9905  absexpzap  9906  nn0abscl  9911  ltabs  9913  lenegsq  9921  recvalap  9923  nnabscl  9926  fzomaxdiflem  9938  fzomaxdif  9939  cau3lem  9940  clim  10032  climconst  10041  climconst2  10042  climuni  10044  climmpt  10051  2clim  10052  climshft2  10057  climcn1  10059  climcn2  10060  mulcn2  10063  climge0  10075  climadd  10076  climmul  10077  climsub  10078  climaddc1  10079  climaddc2  10080  climmulc2  10081  climsubc1  10082  climsubc2  10083  climsqz  10085  climsqz2  10086  clim2iser  10087  clim2iser2  10088  iiserex  10089  iisermulc2  10090  climlec2  10091  iserile  10092  climrecvg1n  10097  dvdsval2  10110  dvdsval3  10111  nndivdvds  10113  moddvds  10116  dvds0lem  10117  absdvdsb  10125  dvdscmulr  10135  dvdsmulcr  10136  modmulconst  10138  dvds2ln  10139  dvdstr  10143  dvdssub2  10148  dvdsadd  10149  dvdsadd2b  10153  dvdslelemd  10154  dvdsleabs2  10157  dvdsabseq  10158  dvdseq  10159  divconjdvds  10160  dvdsflip  10162  dvdsssfz1  10163  dvds1  10164  fzm1ndvds  10167  fzo0dvdseq  10168  mulmoddvds  10174  even2n  10184  mod2eq1n2dvds  10190  evennn02n  10193  evennn2n  10194  2tp1odd  10195  2teven  10198  ltoddhalfle  10204  halfleoddlt  10205  nnehalf  10215  nno  10217  nn0o  10218  nn0ob  10219  pw2dvdseulemle  10234  oddpwdclemdc  10240  oddpwdc  10241  nn0seqcvgd  10242  ialgrlem1st  10243  ialgrlemconst  10244  ialgrp1  10247  algcvgblem  10250  ialgcvga  10252  peano5setOLD  10431  sscoll2  10479  qdencn  10490
  Copyright terms: Public domain W3C validator