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

Theorem simpr 103
Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpr  |-  ( (
ph  /\  ps )  ->  ps )

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 100 1  |-  ( (
ph  /\  ps )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-ia2 100
This theorem is referenced by:  simpri  106  simprd  107  imp  115  adantld  263  ibar  285  pm3.42  315  pm3.4  316  prth  326  sylancom  397  adantll  445  adantrl  447  adantlll  449  adantlrl  451  adantrll  453  adantrrl  455  simpllr  486  simplrr  488  simprlr  490  simprrr  492  anabs7  508  jcab  535  pm4.38  537  pm5.21  611  ioran  669  pm3.14  670  ordi  729  pm4.39  735  pm5.16  737  pm5.54dc  827  intnan  838  intnand  840  dcan  842  bimsc1  870  niabn  874  simp1r  929  simp2r  931  simp3r  933  3anandirs  1238  truanOLD  1261  bilukdc  1287  19.26  1370  exsimpr  1509  19.40  1522  cbvexh  1638  sbequilem  1719  spsbe  1723  cbvexdh  1801  euan  1956  moan  1969  datisi  2010  fresison  2018  rexex  2365  r19.26  2438  r19.40  2461  cbvraldva2  2534  cbvrexdva2  2535  gencbvex  2597  rspct  2646  rspcimdv  2654  rspcimedv  2655  rr19.28v  2680  elrab3t  2694  reu6  2727  rmob  2847  csbiebt  2883  rabssab  3024  ssddif  3168  difin  3171  difrab  3208  preqsn  3543  opprc2  3569  dfnfc2  3595  intmin4  3640  sndisj  3757  exss  3960  euotd  3988  frirrg  4082  suctr  4145  ordtri2or2exmid  4281  tfisi  4288  peano2  4296  relop  4464  releldm  4547  relelrn  4548  resiexg  4631  trin2  4694  xpmlem  4722  unielrel  4823  relcoi2  4826  iota2df  4869  iota2  4871  funopab4  4915  fun11uni  4947  imadiflem  4956  imain  4959  fneq12  4970  f1ssr  5076  fvelrnb  5199  ssimaex  5212  fvmpt2d  5235  fvmptdf  5236  dffo3  5292  ffvresb  5306  fmptco  5308  funfvima3  5370  f1imass  5391  fliftf  5417  fliftval  5418  riota2df  5466  riota5f  5470  acexmidlemcase  5485  ovprc2  5520  eloprabga  5569  eqfnov2  5586  ovmpt2dxf  5604  fnofval  5699  offval2  5704  ofrfval2  5705  caofinvl  5711  2ndrn  5787  1st2ndbr  5788  cnvf1o  5824  f1o2ndf1  5827  mpt2xopoveq  5833  sprmpt2  5835  dftpos4  5856  tpostpos  5857  tposf12  5862  dfsmo2  5880  smores  5885  tfrlem1  5901  tfrlem3ag  5902  tfrlem3a  5903  tfrlemisucaccv  5917  tfrlemi1  5924  tfrexlem  5926  rdgivallem  5946  frecabex  5962  frectfr  5963  frecrdg  5970  freccl  5971  oawordi  6027  nntri3  6053  nndifsnid  6058  nnaordi  6059  nnaordex  6078  nnawordex  6079  nnm00  6080  ersymb  6098  ertr  6099  erref  6104  iserd  6110  swoer  6112  erth  6128  iinerm  6156  erinxp  6158  ecinxp  6159  qsel  6161  qliftel  6164  qliftfun  6166  dom3  6234  ssdomg  6236  cnven  6266  phplem4dom  6302  phpm  6305  phpelm  6306  fidifsnen  6309  fidifsnid  6310  fin0  6320  fientri3  6330  dmaddpqlem  6447  nqpi  6448  mulcanenq  6455  ltaddnq  6477  ltexnqq  6478  prarloclemarch2  6489  ltrnqg  6490  ltnnnq  6493  enq0sym  6502  nqnq0pi  6508  nq0nn  6512  mulcanenq0ec  6515  addnq0mo  6517  mulnq0mo  6518  addnnnq0  6519  prloc  6561  prarloclemlt  6563  prarloclemlo  6564  ltdfpr  6576  genplt2i  6580  genpml  6587  genpmu  6588  addnqprllem  6597  addnqprulem  6598  addnqprl  6599  addnqpru  6600  nqprloc  6615  appdivnq  6633  appdiv0nq  6634  mulnqprl  6638  mulnqpru  6639  distrlem1prl  6652  distrlem1pru  6653  ltprordil  6659  1idprl  6660  1idpru  6661  ltexprlemrl  6680  ltexprlemru  6682  ltexpri  6683  addcanprleml  6684  addcanprlemu  6685  recexprlem1ssl  6703  recexpr  6708  aptiprlemu  6710  archpr  6713  cauappcvgprlemopl  6716  cauappcvgprlemdisj  6721  cauappcvgprlemloc  6722  cauappcvgprlemladdfu  6724  cauappcvgprlemladdfl  6725  cauappcvgprlemladdru  6726  cauappcvgprlemladdrl  6727  caucvgprlemm  6738  caucvgprlemopl  6739  caucvgprlemloc  6745  caucvgprlemladdfu  6747  caucvgprlemladdrl  6748  caucvgprlemlim  6751  caucvgprprlemval  6758  caucvgprprlemml  6764  caucvgprprlemopl  6767  caucvgprprlemopu  6769  caucvgprprlemloc  6773  caucvgprprlemexbt  6776  caucvgprprlemexb  6777  caucvgprprlemaddq  6778  caucvgprprlemlim  6781  addsrmo  6800  mulsrmo  6801  addsrpr  6802  mulsrpr  6803  0idsr  6824  1idsr  6825  recexsrlem  6831  addgt0sr  6832  srpospr  6839  prsradd  6842  prsrlt  6843  caucvgsrlemfv  6847  caucvgsrlemgt1  6851  caucvgsrlemoffval  6852  caucvgsrlemoffcau  6854  caucvgsrlemoffres  6856  rereceu  6935  axarch  6937  nntopi  6940  axcaucvglemval  6943  cnegexlem1  7157  cnegex  7160  negeu  7173  pncan  7188  pncan3  7190  npcan  7191  mulneg1  7362  ltnegcon2  7428  add20  7438  subge0  7439  lesub0  7443  reapval  7534  recexre  7536  apreap  7545  ltmul1a  7549  reapneg  7555  cru  7560  apsym  7564  apcotr  7565  apadd1  7566  apneg  7569  mulext1  7570  apti  7580  gt0ap0  7583  ap0gt0  7596  recexap  7601  rerecclap  7673  recgt0  7783  prodgt0gt0  7784  lemul1a  7791  lemul12a  7795  lt2msq  7819  ltrec1  7821  recreclt  7833  creui  7879  cju  7880  avglt2  8128  un0addcl  8178  nn0ge2m1nn  8205  nn0nndivcl  8207  elnn0z  8221  peano2z  8244  elz2  8275  peano5uzti  8309  zindd  8319  eluzadd  8464  nn0pzuz  8493  eluz2b2  8503  eqreznegel  8512  nn0ge2m1nnALT  8516  divfnzn  8519  qmulz  8521  qapne  8537  qreccl  8538  cnref1o  8544  ge0p1rp  8576  xrltso  8675  z2ge  8697  xltnegi  8706  ixxssixx  8729  lincmb01cmp  8829  iccf1o  8830  fztri3or  8861  fzdcel  8862  fznlem  8863  fzn  8864  uzsubsubfz  8869  fzsplit2  8872  fzopth  8882  fzdifsuc  8901  fzrev2i  8906  elfz1b  8910  fzneuz  8921  fzrevral  8925  ige2m1fz  8930  elfz0ubfz0  8940  elfz0fzfz0  8941  4fvwrd4  8955  2ffzeq  8956  fzospliti  8990  fzosplit  8991  fzo1fzo0n0  8997  fzonmapblen  9001  fzoaddel  9006  fzosubel  9008  fzosubel3  9010  elfzodifsumelfzo  9015  elfzom1elp1fzo  9016  elfzom1p1elfzo  9028  elfzonelfzo  9044  peano2fzor  9046  frec2uzzd  9055  frec2uzuzd  9057  frec2uzrand  9060  frec2uzf1od  9061  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdgfn  9067  frecuzrdgcl  9068  frecuzrdgsuc  9070  frecfzennn  9072  iseqf  9093  iseqss  9095  iseqfeq2  9098  iseqfeq  9100  isermono  9106  iseqsplit  9107  iseqid3s  9115  iseqid  9116  iseqhomo  9117  expivallem  9125  expival  9126  expinnval  9127  expp1  9131  rpexpcl  9143  expaddzaplem  9167  leexp1a  9178  exple1  9179  subsq  9227  binom2  9231  binom3  9235  bernneq3  9240  expnbnd  9241  shftfvalg  9288  ovshftex  9289  shftdm  9292  shftfib  9293  shftval  9295  shftval5  9299  shftf  9300  2shfti  9301  crre  9326  rereb  9332  cjreim2  9373  cjap  9375  caucvgrelemrec  9447  caucvgrelemcau  9448  caucvgre  9449  cvg1nlemf  9451  cvg1nlemres  9453  uzin2  9455  rexuz3  9457  recvguniq  9462  sqrt0  9471  resqrexlemdecn  9479  resqrexlemlo  9480  resqrexlemcalc3  9483  resqrexlemnm  9485  resqrexlemcvg  9486  resqrexlemoverl  9488  resqrexlemglsq  9489  resqrexlemga  9490  resqrex  9493  sqrtgt0  9501  absrpclap  9528  absext  9530  absmul  9536  leabs  9541  nn0abscl  9550  ltabs  9552  abslt  9553  absle  9554  abssubap0  9555  abstri  9569  cau3lem  9579  caubnd2  9582  clim  9670  climi2  9677  climconst2  9680  climuni  9682  climmpt  9689  climshftlemg  9691  climres  9692  climcn1  9697  subcn2  9700  cn1lem  9702  climadd  9714  climmul  9715  climsub  9716  climle  9722  climsqz  9723  climsqz2  9724  clim2iser  9725  clim2iser2  9726  iiserex  9727  iisermulc2  9728  iserile  9730  iserige0  9731  climub  9732  climserile  9733  climrecvg1n  9735  climcvg1nlem  9736  serif0  9739  sqrt2irr  9746  ialgrp1  9753  ialgcvga  9758  bj-indind  9920  bj-omtrans  9945
  Copyright terms: Public domain W3C validator