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

Theorem simpr 108
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 ((𝜑𝜓) → 𝜓)

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 105 1 ((𝜑𝜓) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-ia2 105
This theorem is referenced by:  simpri  111  simprd  112  imp  122  adantld  272  ibar  295  pm3.42  325  pm3.4  326  prth  336  simpl2im  378  sylancom  411  adantll  460  adantrl  462  adantlll  464  adantlrl  466  adantrll  468  adantrrl  470  simpllr  501  simplrr  503  simprlr  505  simprrr  507  anabs7  539  jcab  568  pm4.38  570  pm5.21  644  ioran  702  pm3.14  703  ordi  763  pm4.39  769  pm5.16  771  pm5.54dc  861  intnan  872  intnand  874  dcan  876  bimsc1  905  niabn  909  simp1r  964  simp2r  966  simp3r  968  3anandirs  1280  bilukdc  1328  19.26  1411  exsimpr  1550  19.40  1563  cbvexh  1679  sbequilem  1760  spsbe  1764  cbvexdh  1843  euan  1998  moan  2011  datisi  2052  fresison  2060  rexex  2411  r19.26  2486  r19.40  2509  cbvraldva2  2582  cbvrexdva2  2583  gencbvex  2646  rspct  2695  rspcimdv  2703  rspcimedv  2704  rr19.28v  2735  elrab3t  2749  reu6  2782  rmob  2907  csbiebt  2943  rabssab  3082  ssddif  3205  difin  3208  difrab  3245  preqsn  3575  opprc2  3601  dfnfc2  3627  intmin4  3672  sndisj  3789  exss  3990  euotd  4017  frirrg  4113  suctr  4184  ordtri2or2exmid  4322  wetriext  4327  reg3exmidlemwe  4329  tfisi  4336  peano2  4344  relop  4514  releldm  4597  relelrn  4598  resiexg  4683  trin2  4746  xpmlem  4774  unielrel  4875  relcoi2  4878  iota2df  4921  iota2  4923  funopab4  4967  fun11uni  5000  imadiflem  5009  imain  5012  fneq12  5023  f1ssr  5129  fvelrnb  5253  ssimaex  5266  fvmpt2d  5289  fvmptdf  5290  dffo3  5346  ffvresb  5360  fmptco  5362  funfvima3  5424  f1imass  5445  fliftf  5470  fliftval  5471  riota2df  5519  riota5f  5523  acexmidlemcase  5538  ovprc2  5573  eloprabga  5622  eqfnov2  5639  ovmpt2dxf  5657  fnofval  5752  offval2  5757  ofrfval2  5758  caofinvl  5764  2ndrn  5840  1st2ndbr  5841  cnvf1o  5877  f1o2ndf1  5880  mpt2xopoveq  5889  sprmpt2  5891  dftpos4  5912  tpostpos  5913  tposf12  5918  dfsmo2  5936  smores  5941  tfrlem1  5957  tfrlem3ag  5958  tfrlem3a  5959  tfrlemisucaccv  5974  tfrlemi1  5981  tfrexlem  5983  tfr1onlem3ag  5986  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemaccex  5997  tfr1onlemres  5998  tfri1dALT  6000  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemaccex  6010  tfrcllemres  6011  tfrcl  6013  rdgivallem  6030  rdgon  6035  frecabex  6047  frecabcl  6048  frectfr  6049  frecrdg  6057  oawordi  6113  nntri3  6141  nndifsnid  6146  nnaordi  6147  nnaordex  6166  nnawordex  6167  nnm00  6168  ersymb  6186  ertr  6187  erref  6192  iserd  6198  swoer  6200  erth  6216  iinerm  6244  erinxp  6246  ecinxp  6247  qsel  6249  qliftel  6252  qliftfun  6254  dom3  6323  ssdomg  6325  cnven  6355  xpen  6386  phplem4dom  6397  phpm  6400  phpelm  6401  fidifsnen  6405  fidifsnid  6406  fin0  6419  fin0or  6420  en2eqpr  6434  fientri3  6435  unsnfidcex  6440  unsnfidcel  6441  unfidisj  6442  undiffi  6443  unfiin  6444  fnfi  6446  relcnvfi  6449  f1dmvrnfibi  6452  suplubti  6472  suplub2ti  6473  supelti  6474  supisolem  6480  supisoex  6481  infglbti  6497  ordiso2  6505  en2eleq  6521  en2other2  6522  dmaddpqlem  6629  nqpi  6630  mulcanenq  6637  ltaddnq  6659  ltexnqq  6660  prarloclemarch2  6671  ltrnqg  6672  ltnnnq  6675  enq0sym  6684  nqnq0pi  6690  nq0nn  6694  mulcanenq0ec  6697  addnq0mo  6699  mulnq0mo  6700  addnnnq0  6701  prloc  6743  prarloclemlt  6745  prarloclemlo  6746  ltdfpr  6758  genplt2i  6762  genpml  6769  genpmu  6770  addnqprllem  6779  addnqprulem  6780  addnqprl  6781  addnqpru  6782  nqprloc  6797  appdivnq  6815  appdiv0nq  6816  mulnqprl  6820  mulnqpru  6821  distrlem1prl  6834  distrlem1pru  6835  ltprordil  6841  1idprl  6842  1idpru  6843  ltexprlemrl  6862  ltexprlemru  6864  ltexpri  6865  addcanprleml  6866  addcanprlemu  6867  recexprlem1ssl  6885  recexpr  6890  aptiprlemu  6892  archpr  6895  cauappcvgprlemopl  6898  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  caucvgprlemm  6920  caucvgprlemopl  6921  caucvgprlemloc  6927  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlemlim  6933  caucvgprprlemval  6940  caucvgprprlemml  6946  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemexbt  6958  caucvgprprlemexb  6959  caucvgprprlemaddq  6960  caucvgprprlemlim  6963  addsrmo  6982  mulsrmo  6983  addsrpr  6984  mulsrpr  6985  0idsr  7006  1idsr  7007  recexsrlem  7013  addgt0sr  7014  srpospr  7021  prsradd  7024  prsrlt  7025  caucvgsrlemfv  7029  caucvgsrlemgt1  7033  caucvgsrlemoffval  7034  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  rereceu  7117  axarch  7119  nntopi  7122  axcaucvglemval  7125  muladd11r  7331  cnegexlem1  7350  cnegex  7353  negeu  7366  pncan  7381  pncan3  7383  npcan  7384  addid0  7544  negf1o  7553  mulneg1  7566  lelttrdi  7597  ltnegcon2  7635  add20  7645  subge0  7646  lesub0  7650  reapval  7743  recexre  7745  apreap  7754  ltmul1a  7758  reapneg  7764  cru  7769  apsym  7773  apcotr  7774  apadd1  7775  apneg  7778  mulext1  7779  apti  7789  gt0ap0  7792  ap0gt0  7805  recexap  7810  divmulassap  7850  divmulasscomap  7851  rerecclap  7885  recgt0  7995  prodgt0gt0  7996  lemul1a  8003  lemul12a  8007  lt2msq  8031  ltrec1  8033  recreclt  8045  negiso  8100  creui  8104  cju  8105  avglt2  8337  un0addcl  8388  nn0ge2m1nn  8415  nn0nndivcl  8417  elnn0z  8445  peano2z  8468  elz2  8500  suprzclex  8526  peano5uzti  8536  zindd  8546  eluzadd  8728  nn0pzuz  8756  supinfneg  8764  infsupneg  8765  eluz2b2  8771  eqreznegel  8780  nn0ge2m1nnALT  8784  divfnzn  8787  qmulz  8789  qapne  8805  qreccl  8808  cnref1o  8814  ge0p1rp  8846  xrltso  8947  z2ge  8969  xltnegi  8978  ixxssixx  9001  lincmb01cmp  9101  iccf1o  9102  zltaddlt1le  9104  fztri3or  9134  fzdcel  9135  fznlem  9136  fzn  9137  uzsubsubfz  9142  fzsplit2  9145  fzopth  9155  fzdifsuc  9174  fzrev2i  9179  elfz1b  9183  fzneuz  9194  fzrevral  9198  ige2m1fz  9203  elfz0ubfz0  9213  elfz0fzfz0  9214  4fvwrd4  9227  2ffzeq  9228  fzospliti  9262  fzosplit  9263  fzo1fzo0n0  9269  fzonmapblen  9273  fzoaddel  9278  fzosubel  9280  fzosubel3  9282  elfzodifsumelfzo  9287  elfzom1elp1fzo  9288  elfzom1p1elfzo  9300  elfzonelfzo  9316  peano2fzor  9318  exfzdc  9326  fvinim0ffz  9327  qtri3or  9329  exbtwnzlemstep  9334  rebtwn2zlemstep  9339  qbtwnxr  9344  apbtwnz  9356  flqge  9364  flqltnz  9369  flqaddz  9379  btwnzge0  9382  flltdivnn0lt  9386  intfracq  9402  flqdiv  9403  modqid0  9432  q0mod  9437  q1mod  9438  modqmuladdim  9449  modqmuladdnn0  9450  q2txmodxeq0  9466  q2submod  9467  modifeq2int  9468  modqsubdir  9475  modsumfzodifsn  9478  addmodlteq  9480  frec2uzzd  9482  frec2uzuzd  9484  frec2uzrand  9487  frec2uzf1od  9488  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgg  9498  frecuzrdgdomlem  9499  frecuzrdgfunlem  9501  frecuzrdgsuctlem  9505  frecfzennn  9508  uzsinds  9518  iseqvalt  9532  iseqoveq  9540  iseqss  9541  iseqsst  9542  iseqfeq2  9545  iseqfeq  9547  isermono  9553  iseqsplit  9554  iseqid3s  9562  iseqid  9563  iseqhomo  9565  iseqz  9566  expivallem  9574  expival  9575  expinnval  9576  expp1  9580  rpexpcl  9592  expaddzaplem  9616  leexp1a  9628  exple1  9629  subsq  9678  binom2  9682  binom3  9687  bernneq3  9692  expnbnd  9693  expcan  9741  nn0opthd  9746  faclbnd  9765  faclbnd6  9768  facubnd  9769  facavg  9770  bcval  9773  bccmpl  9778  ibcval5  9787  bcpasc  9790  sizeennnuni  9803  sizeennn  9804  sizefiv01gt1  9806  sizeeqf1oi  9812  sizenncl  9820  fseq1size  9825  shftfvalg  9844  ovshftex  9845  shftdm  9848  shftfib  9849  shftval  9851  shftval5  9855  shftf  9856  2shfti  9857  crre  9882  rereb  9888  cjreim2  9929  cjap  9931  caucvgrelemrec  10003  caucvgrelemcau  10004  caucvgre  10005  cvg1nlemf  10007  cvg1nlemres  10009  uzin2  10011  rexuz3  10014  recvguniq  10019  sqrt0  10028  resqrexlemdecn  10036  resqrexlemlo  10037  resqrexlemcalc3  10040  resqrexlemnm  10042  resqrexlemcvg  10043  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemga  10047  resqrex  10050  sqrtgt0  10058  absrpclap  10085  absext  10087  absmul  10093  leabs  10098  nn0abscl  10109  ltabs  10111  abslt  10112  absle  10113  abssubap0  10114  abstri  10128  cau3lem  10138  caubnd2  10141  maxabsle  10228  maxabslemlub  10231  maxabslemval  10232  maxcl  10234  maxleastb  10238  maxltsup  10242  rexanre  10244  rexico  10245  fimaxre2  10247  minmax  10250  min2inf  10252  clim  10258  climi2  10265  climconst2  10268  climuni  10270  climmpt  10277  climshftlemg  10279  climres  10280  climcn1  10285  subcn2  10288  cn1lem  10290  climadd  10302  climmul  10303  climsub  10304  climle  10310  climsqz  10311  climsqz2  10312  clim2iser  10313  clim2iser2  10314  iiserex  10315  iisermulc2  10316  iserile  10318  iserige0  10319  climub  10320  climserile  10321  climrecvg1n  10323  climcvg1nlem  10324  serif0  10327  sumeq2d  10334  sumeq2  10335  isumrblem  10337  fisumcvg  10338  isumrb  10339  dvdsval2  10343  dvdsdc  10348  moddvds  10349  zdvdsdc  10361  dvdscmul  10367  dvdsmulc  10368  dvdscmulr  10369  dvdsmulcr  10370  modmulconst  10372  dvdsadd  10383  dvdsadd2b  10387  dvdslelemd  10388  dvdsle  10389  dvdsabseq  10392  dvdseq  10393  divconjdvds  10394  dvds1  10398  fzo0dvdseq  10402  dvdsmod  10407  oddm1even  10419  mod2eq1n2dvds  10423  evennn02n  10426  evennn2n  10427  divalglemnn  10462  divalglemnqt  10464  divalglemeunn  10465  divalglemex  10466  divalglemeuneg  10467  divalg  10468  divalgmod  10471  modremain  10473  infssuzex  10489  gcdsupex  10493  gcdsupcl  10494  gcdval  10495  dvdslegcd  10500  gcdnncl  10503  gcdneg  10517  gcdaddm  10519  gcd1  10522  bezoutlemnewy  10529  bezoutlemmain  10531  bezoutlemex  10534  bezoutlemzz  10535  bezoutlemaz  10536  bezoutlembz  10537  bezoutlembi  10538  bezoutlemle  10541  bezoutlemsup  10542  gcdass  10548  gcdzeq  10555  dvdsmulgcd  10558  bezoutr1  10566  ialgrp1  10572  ialgcvga  10577  eucalgval2  10579  eucalgf  10581  eucalglt  10583  lcmval  10589  lcmledvds  10596  lcmneg  10600  lcmgcd  10604  lcmid  10606  coprmgcdb  10614  ncoprmgcdne1b  10615  mulgcddvds  10620  rpmulgcd2  10621  qredeq  10622  divgcdcoprm0  10627  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  isprm2lem  10642  prmind2  10646  sqnprm  10661  isprm6  10670  prmdvdsexp  10671  prmfac1  10675  rpexp  10676  rpexp1i  10677  sqrt2irr  10685  pw2dvdslemn  10687  pw2dvdseulemle  10689  oddpwdclemxy  10691  oddpwdclemdc  10695  oddpwdc  10696  znege1  10700  sqrt2irraplemnn  10701  sqrt2irrap  10702  oddennn  10703  evenennn  10704  bj-indind  10885  bj-omtrans  10909  qdencn  10943
  Copyright terms: Public domain W3C validator