Theorem simpr 109

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

Step	Hyp	Ref	Expression
1		ax-ia2 106	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-ia2 106

This theorem is referenced by:  simpri  112  simprd  113  imp  123  adantld  274  ibar  297  pm3.42  328  pm3.4  329  prth  339  simpl2im  381  sylancom  414  adantll  465  adantrl  467  adantlll  469  adantlrl  471  adantrll  473  adantrrl  475  simpllr  506  simplrr  508  simprlr  510  simprrr  512  anabs7  546  jcab  575  pm4.38  577  pm5.21  667  ioran  724  pm3.14  725  ordi  788  pm4.39  794  pm5.16  796  pm5.54dc  886  intnan  897  intnand  899  dcan  901  bimsc1  930  niabn  934  simp1r  989  simp2r  991  simp3r  993  3anandirs  1309  bilukdc  1357  19.26  1440  exsimpr  1580  19.40  1593  cbvexh  1711  sbequilem  1792  spsbe  1796  cbvexdh  1876  euan  2031  moan  2044  datisi  2085  fresison  2093  rexex  2453  r19.26  2532  r19.29an  2548  r19.40  2559  cbvraldva2  2632  cbvrexdva2  2633  gencbvex  2703  rspct  2753  rspcimdv  2761  rspcimedv  2762  rr19.28v  2794  elrab3t  2808  reu6  2842  rmob  2969  csbiebt  3005  rabssab  3150  ssddif  3276  difin  3279  difrab  3316  dcun  3439  eqifdc  3472  ifmdc  3475  preqsn  3668  opprc2  3694  dfnfc2  3720  intmin4  3765  sndisj  3891  undifexmid  4077  exmid01  4081  pwntru  4082  exmidn0m  4084  exmidsssn  4085  exmidsssnc  4086  exmidundif  4089  exmidundifim  4090  exss  4109  euotd  4136  frirrg  4232  suctr  4303  abnexg  4327  ordtri2or2exmid  4446  wetriext  4451  reg3exmidlemwe  4453  tfisi  4461  peano2  4469  omsinds  4495  nnpredcl  4496  relop  4649  releldm  4734  relelrn  4735  resiexg  4822  trin2  4888  xpmlem  4917  unielrel  5024  relcoi2  5027  iota2df  5070  iota2  5072  funopab4  5118  fun11uni  5151  imadiflem  5160  imain  5163  fneq12  5174  f1ssr  5293  fvelrnb  5423  ssimaex  5436  fvmpt2d  5461  fvmptdf  5462  dffo3  5521  ffvresb  5537  fmptco  5540  funfvima3  5605  f1imass  5629  fliftf  5654  fliftval  5655  riota2df  5704  riota5f  5708  acexmidlemcase  5723  ovprc2  5762  eloprabga  5812  eqfnov2  5832  ovmpodxf  5850  ofvalg  5945  offval2  5951  ofrfval2  5952  caofinvl  5958  2ndrn  6035  1st2ndbr  6036  cnvf1o  6076  f1o2ndf1  6079  mpoxopoveq  6091  dftpos4  6114  tpostpos  6115  tposf12  6120  dfsmo2  6138  smores  6143  tfrlem1  6159  tfrlem3ag  6160  tfrlem3a  6161  tfrlemisucaccv  6176  tfrlemi1  6183  tfrexlem  6185  tfr1onlem3ag  6188  tfr1onlemsucaccv  6192  tfr1onlembxssdm  6194  tfr1onlembfn  6195  tfr1onlemaccex  6199  tfr1onlemres  6200  tfri1dALT  6202  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  tfrcllembfn  6208  tfrcllemaccex  6212  tfrcllemres  6213  tfrcl  6215  rdgivallem  6232  rdgon  6237  frecabex  6249  frecabcl  6250  frectfr  6251  frecrdg  6259  oawordi  6319  nntri3  6347  nntr2  6353  dcdifsnid  6354  nnaordi  6358  nnaordex  6377  nnawordex  6378  nnm00  6379  ersymb  6397  ertr  6398  erref  6403  iserd  6409  swoer  6411  erth  6427  iinerm  6455  erinxp  6457  ecinxp  6458  qsel  6460  qliftel  6463  qliftfun  6465  fvdiagfn  6541  ixpssmapg  6576  resixp  6581  mptelixpg  6582  dom3  6624  ssdomg  6626  cnven  6656  xpen  6692  xpmapenlem  6696  ssenen  6698  phplem4dom  6709  phpm  6712  phpelm  6713  fidifsnen  6717  fin0  6732  fin0or  6733  isinfinf  6744  tridc  6746  fimax2gtrilemstep  6747  fimax2gtri  6748  finexdc  6749  en2eqpr  6754  fientri3  6756  unsnfidcex  6761  unsnfidcel  6762  unfidisj  6763  undifdcss  6764  undifdc  6765  unfiin  6767  fiintim  6770  fnfi  6777  relcnvfi  6781  f1dmvrnfibi  6784  iunfidisj  6786  f1finf1o  6787  fidcenumlemrks  6793  fidcenumlemr  6795  fidcenum  6796  fival  6810  elfi2  6812  ssfii  6814  fiss  6817  suplubti  6839  suplub2ti  6840  supelti  6841  supisolem  6847  supisoex  6848  infglbti  6864  ordiso2  6872  djuss  6907  updjudhcoinlf  6917  updjudhcoinrg  6918  updjud  6919  djudom  6930  omp1eomlem  6931  difinfsnlem  6936  difinfsn  6937  difinfinf  6938  ctm  6946  ctssdclemn0  6947  ctssdccl  6948  ctssdc  6950  enumctlemm  6951  enumct  6952  enomnilem  6960  finomni  6962  exmidomni  6964  fodjuomnilemdc  6966  fodjuomnilemres  6970  nnnninf  6973  ctssexmid  6974  ismkvnex  6979  mkvprop  6982  fodjumkvlemres  6983  en2eleq  6999  en2other2  7000  exmidfodomrlemeldju  7003  exmidfodomrlemreseldju  7004  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  exmidaclem  7012  dju1en  7017  djudomr  7024  dmaddpqlem  7133  nqpi  7134  mulcanenq  7141  ltaddnq  7163  ltexnqq  7164  prarloclemarch2  7175  ltrnqg  7176  ltnnnq  7179  enq0sym  7188  nqnq0pi  7194  nq0nn  7198  mulcanenq0ec  7201  addnq0mo  7203  mulnq0mo  7204  addnnnq0  7205  prloc  7247  prarloclemlt  7249  prarloclemlo  7250  ltdfpr  7262  genplt2i  7266  genpml  7273  genpmu  7274  addnqprllem  7283  addnqprulem  7284  addnqprl  7285  addnqpru  7286  nqprloc  7301  appdivnq  7319  appdiv0nq  7320  mulnqprl  7324  mulnqpru  7325  distrlem1prl  7338  distrlem1pru  7339  ltprordil  7345  1idprl  7346  1idpru  7347  ltexprlemrl  7366  ltexprlemru  7368  ltexpri  7369  addcanprleml  7370  addcanprlemu  7371  recexprlem1ssl  7389  recexpr  7394  aptiprlemu  7396  archpr  7399  cauappcvgprlemopl  7402  cauappcvgprlemdisj  7407  cauappcvgprlemloc  7408  cauappcvgprlemladdfu  7410  cauappcvgprlemladdfl  7411  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprlemm  7424  caucvgprlemopl  7425  caucvgprlemloc  7431  caucvgprlemladdfu  7433  caucvgprlemladdrl  7434  caucvgprlemlim  7437  caucvgprprlemval  7444  caucvgprprlemml  7450  caucvgprprlemopl  7453  caucvgprprlemopu  7455  caucvgprprlemloc  7459  caucvgprprlemexbt  7462  caucvgprprlemexb  7463  caucvgprprlemaddq  7464  caucvgprprlemlim  7467  addsrmo  7486  mulsrmo  7487  addsrpr  7488  mulsrpr  7489  0idsr  7510  1idsr  7511  recexsrlem  7517  addgt0sr  7518  srpospr  7525  prsradd  7528  prsrlt  7529  caucvgsrlemfv  7533  caucvgsrlemgt1  7537  caucvgsrlemoffval  7538  caucvgsrlemoffcau  7540  caucvgsrlemoffres  7542  rereceu  7624  axarch  7626  nntopi  7629  axcaucvglemval  7632  muladd11r  7841  cnegexlem1  7860  cnegex  7863  negeu  7876  pncan  7891  pncan3  7893  npcan  7894  addid0  8054  negf1o  8063  mulneg1  8076  lelttrdi  8107  ltnegcon2  8145  add20  8155  subge0  8156  lesub0  8160  reapval  8256  recexre  8258  apreap  8267  ltmul1a  8271  reapneg  8277  cru  8282  apsym  8286  apcotr  8287  apadd1  8288  apneg  8291  mulext1  8292  apti  8302  gt0ap0  8306  ap0gt0  8319  subap0  8322  recexap  8327  divmulassap  8368  divmulasscomap  8369  rerecclap  8403  recgt0  8518  prodgt0gt0  8519  lemul1a  8526  lemul12a  8530  lt2msq  8554  ltrec1  8556  recreclt  8568  negiso  8623  sup3exmid  8625  creui  8628  cju  8629  avglt2  8863  un0addcl  8914  nn0ge2m1nn  8941  nn0nndivcl  8943  elnn0z  8971  peano2z  8994  elz2  9026  suprzclex  9053  peano5uzti  9063  zindd  9073  btwnapz  9085  eluzadd  9256  nn0pzuz  9284  supinfneg  9292  infsupneg  9293  eluz2b2  9299  eqreznegel  9308  nn0ge2m1nnALT  9312  divfnzn  9315  qmulz  9317  qapne  9333  qreccl  9336  cnref1o  9342  ge0p1rp  9374  xrltso  9475  npnflt  9491  nmnfgt  9494  z2ge  9502  xltnegi  9511  xaddval  9521  xaddcom  9537  xnegdi  9544  xaddass  9545  xpncan  9547  xleadd1a  9549  xltadd1  9552  xlt2add  9556  xsubge0  9557  xposdif  9558  xlesubadd  9559  xleaddadd  9563  ixxssixx  9578  lincmb01cmp  9679  iccf1o  9680  zltaddlt1le  9682  fztri3or  9712  fzdcel  9713  fznlem  9714  fzn  9715  uzsubsubfz  9720  fzsplit2  9723  fzopth  9734  fzdifsuc  9754  fzrev2i  9759  elfz1b  9763  fzneuz  9774  fzrevral  9778  ige2m1fz  9783  elfz0ubfz0  9795  elfz0fzfz0  9796  4fvwrd4  9810  2ffzeq  9811  fzospliti  9846  fzosplit  9847  fzo1fzo0n0  9853  fzonmapblen  9857  fzoaddel  9862  fzosubel  9864  fzosubel3  9866  elfzodifsumelfzo  9871  elfzom1elp1fzo  9872  elfzom1p1elfzo  9884  elfzonelfzo  9900  peano2fzor  9902  exfzdc  9910  fvinim0ffz  9911  qtri3or  9913  exbtwnzlemstep  9918  rebtwn2zlemstep  9923  qbtwnxr  9928  apbtwnz  9940  flqge  9948  flqltnz  9953  flqaddz  9963  btwnzge0  9966  flltdivnn0lt  9970  intfracq  9986  flqdiv  9987  modqid0  10016  q0mod  10021  q1mod  10022  modqmuladdim  10033  modqmuladdnn0  10034  q2txmodxeq0  10050  q2submod  10051  modifeq2int  10052  modqsubdir  10059  modsumfzodifsn  10062  addmodlteq  10064  frec2uzzd  10066  frec2uzuzd  10068  frec2uzrand  10071  frec2uzf1od  10072  frecuzrdgrrn  10074  frec2uzrdg  10075  frecuzrdgtcl  10078  frecuzrdgsuc  10080  frecuzrdgg  10082  frecuzrdgdomlem  10083  frecuzrdgfunlem  10085  frecuzrdgsuctlem  10089  frecfzennn  10092  uzsinds  10108  seq3val  10124  seqvalcd  10125  seq3clss  10133  seq3feq2  10136  seq3feq  10138  ser3mono  10144  seq3split  10145  iseqf1olemkle  10150  iseqf1olemklt  10151  iseqf1olemqcl  10152  iseqf1olemnab  10154  iseqf1olemab  10155  iseqf1olemqf  10157  iseqf1olemmo  10158  iseqf1olemqf1o  10159  iseqf1olemqk  10160  iseqf1olemjpcl  10161  iseqf1olemqpcl  10162  iseqf1olemfvp  10163  seq3f1olemqsumkj  10164  seq3f1olemqsumk  10165  seq3f1olemqsum  10166  seq3f1oleml  10169  seq3f1o  10170  seq3id3  10173  seq3id  10174  seq3homo  10176  seq3z  10177  seqfeq3  10178  fser0const  10182  ser3ge0  10183  exp3vallem  10187  exp3val  10188  expnnval  10189  expp1  10193  rpexpcl  10205  expaddzaplem  10229  leexp1a  10241  exple1  10242  subsq  10292  binom2  10296  binom3  10302  bernneq3  10307  expnbnd  10308  expcan  10356  nn0opthd  10361  faclbnd  10380  faclbnd6  10383  facubnd  10384  facavg  10385  bcval  10388  bccmpl  10393  bcval5  10402  bcpasc  10405  hashennnuni  10418  hashennn  10419  hashfiv01gt1  10421  fihasheqf1oi  10427  hashnncl  10435  fseq1hash  10440  fiprsshashgt1  10456  fimaxq  10466  fnfz0hash  10468  ffzo0hash  10470  zfz1isolemiso  10475  zfz1iso  10477  seq3coll  10478  shftfvalg  10483  ovshftex  10484  shftdm  10487  shftfib  10488  shftval  10490  shftval5  10494  shftf  10495  2shfti  10496  seq3shft  10503  crre  10522  rereb  10528  cjreim2  10569  cjap  10571  caucvgrelemrec  10643  caucvgrelemcau  10644  caucvgre  10645  cvg1nlemf  10647  cvg1nlemres  10649  uzin2  10651  rexuz3  10654  recvguniq  10659  sqrt0  10668  resqrexlemdecn  10676  resqrexlemlo  10677  resqrexlemcalc3  10680  resqrexlemnm  10682  resqrexlemcvg  10683  resqrexlemoverl  10685  resqrexlemglsq  10686  resqrexlemga  10687  resqrex  10690  sqrtgt0  10698  absrpclap  10725  absext  10727  absmul  10733  leabs  10738  nn0abscl  10749  ltabs  10751  abslt  10752  absle  10753  abssubap0  10754  abstri  10768  cau3lem  10778  caubnd2  10781  maxabsle  10868  maxabslemlub  10871  maxabslemval  10872  maxcl  10874  maxleastb  10878  maxltsup  10882  rexanre  10884  rexico  10885  zmaxcl  10888  2zsupmax  10889  fimaxre2  10890  minmax  10893  min2inf  10896  minabs  10899  minclpr  10900  mul0inf  10904  xrmaxiflemcl  10906  xrmaxifle  10907  xrmaxiflemab  10908  xrmaxiflemlub  10909  xrmaxiflemcom  10910  xrmaxiflemval  10911  xrltmaxsup  10918  xrmaxltsup  10919  xrmaxaddlem  10921  xrmaxadd  10922  xrnegiso  10923  xrminmax  10926  xrbdtri  10937  clim  10942  climi2  10949  climconst2  10952  climuni  10954  climmpt  10961  climshftlemg  10963  climres  10964  climcn1  10969  subcn2  10972  cn1lem  10975  climadd  10987  climmul  10988  climsub  10989  climle  10995  climsqz  10996  climsqz2  10997  clim2ser  10998  clim2ser2  10999  iserex  11000  isermulc2  11001  iserle  11003  iserge0  11004  climub  11005  climrecvg1n  11009  climcvg1nlem  11010  serf0  11013  sumeq2  11020  sumfct  11035  sumrbdclem  11037  fsum3cvg  11038  sumrbdc  11039  summodclem2a  11042  summodclem2  11043  summodc  11044  zsumdc  11045  isum  11046  fsum3  11048  sum0  11049  isumz  11050  fsumf1o  11051  isumss  11052  fisumss  11053  isumss2  11054  fsum3cvg2  11055  fsum3cvg3  11057  fsum3ser  11058  fsumcl2lem  11059  fsumcllem  11060  fsumadd  11067  fsumsplit  11068  sumsnf  11070  isumclim3  11084  isummulc2  11087  isumadd  11092  fsum2dlemstep  11095  fsum2d  11096  fisumcom2  11099  fsum0diaglem  11101  fsumrev  11104  fsumshft  11105  fisumrev2  11107  fsummulc2  11109  fsumconst  11115  modfsummod  11119  fsum00  11123  fsumabs  11126  telfsumo  11127  fsumparts  11131  fsumrelem  11132  iserabs  11136  cvgcmpub  11137  fsumiun  11138  binom1dif  11148  bcxmas  11150  isumshft  11151  isumlessdc  11157  divcnv  11158  trireciplem  11161  trirecip  11162  expcnvap0  11163  expcnvre  11164  expcnv  11165  explecnv  11166  geolim  11172  geolim2  11173  geo2sum  11175  geo2lim  11177  geoisum  11178  geoisumr  11179  geoisum1  11180  geoisum1c  11181  cvgratnnlemnexp  11185  cvgratnnlemseq  11187  cvgratz  11193  mertenslem2  11197  mertensabs  11198  eftvalcn  11214  ef0lem  11217  efcvgfsum  11224  ege2le3  11228  efcj  11230  efaddlem  11231  efadd  11232  eftlcvg  11244  eftlub  11247  efler  11256  eflegeo  11259  tanvalap  11266  tanclap  11267  tanval2ap  11271  tanval3ap  11272  tannegap  11286  sinadd  11294  cosadd  11295  eirrap  11332  dvdsval2  11344  dvdsdc  11349  moddvds  11350  zdvdsdc  11362  dvdscmul  11368  dvdsmulc  11369  dvdscmulr  11370  dvdsmulcr  11371  modmulconst  11373  dvdsadd  11384  dvdsadd2b  11388  dvdslelemd  11389  dvdsle  11390  dvdsabseq  11393  dvdseq  11394  divconjdvds  11395  dvds1  11399  fzo0dvdseq  11403  dvdsmod  11408  oddm1even  11420  mod2eq1n2dvds  11424  evennn02n  11427  evennn2n  11428  divalglemnn  11463  divalglemnqt  11465  divalglemeunn  11466  divalglemex  11467  divalglemeuneg  11468  divalg  11469  divalgmod  11472  modremain  11474  infssuzex  11490  gcdsupex  11494  gcdsupcl  11495  gcdval  11496  dvdslegcd  11501  gcdnncl  11504  gcdneg  11518  gcdaddm  11520  gcd1  11523  bezoutlemnewy  11530  bezoutlemmain  11532  bezoutlemex  11535  bezoutlemzz  11536  bezoutlemaz  11537  bezoutlembz  11538  bezoutlembi  11539  bezoutlemle  11542  bezoutlemsup  11543  gcdass  11549  gcdzeq  11556  dvdsmulgcd  11559  bezoutr1  11567  algrp1  11573  algcvga  11578  eucalgval2  11580  eucalgf  11582  eucalglt  11584  lcmval  11590  lcmledvds  11597  lcmneg  11601  lcmgcd  11605  lcmid  11607  coprmgcdb  11615  ncoprmgcdne1b  11616  mulgcddvds  11621  rpmulgcd2  11622  qredeq  11623  divgcdcoprm0  11628  divgcdcoprmex  11629  cncongr1  11630  cncongr2  11631  isprm2lem  11643  prmind2  11647  sqnprm  11662  isprm6  11671  prmdvdsexp  11672  prmfac1  11676  rpexp  11677  rpexp1i  11678  sqrt2irr  11686  pw2dvdslemn  11688  pw2dvdseulemle  11690  oddpwdclemxy  11692  oddpwdclemdc  11696  oddpwdc  11697  znege1  11701  sqrt2irraplemnn  11702  sqrt2irrap  11703  divnumden  11719  qden1elz  11728  phibndlem  11737  dfphi2  11741  phiprmpw  11743  crth  11745  phimullem  11746  oddennn  11750  evenennn  11751  ennnfonelemk  11758  ennnfonelemg  11761  ennnfonelemss  11768  ennnfoneleminc  11769  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemex  11772  ennnfonelemhom  11773  ennnfonelemrnh  11774  ennnfonelemfun  11775  ennnfonelemf1  11776  ennnfonelemrn  11777  ennnfonelemdm  11778  ennnfonelemnn0  11780  exmidunben  11784  ctinfomlemom  11785  ctinfom  11786  ctinf  11788  ctiunctlemudc  11793  ctiunctlemf  11794  ctiunct  11796  unct  11797  isstruct2im  11812  isstruct2r  11813  setsvalg  11832  setsslid  11852  ressid2  11861  ressval2  11862  2strbasg  11903  2stropg  11904  2strop1g  11907  restval  11969  restid2  11972  eltg3i  12068  bastg  12073  topbas  12079  tgtop  12080  tgidm  12086  tgss2  12091  bastop2  12096  epttop  12102  iuncld  12127  clsss2  12141  isopn3i  12147  neiint  12157  neii2  12161  neissex  12177  restbasg  12180  tgrest  12181  resttopon  12183  ssrest  12194  restopn2  12195  lmfval  12204  cnpval  12209  lmcvg  12228  iscnp4  12229  cncnpi  12239  cnconst2  12244  cnrest  12246  cnrest2  12247  cnrest2r  12248  cnptopresti  12249  cnptoprest  12250  cnptoprest2  12251  lmss  12257  lmtopcnp  12261  txcnp  12282  upxp  12283  uptx  12285  txcn  12286  txlm  12290  cnmpt11  12294  cnmpt1t  12296  psmetres2  12322  ismet2  12343  xmettri2  12350  xmetres2  12368  metres2  12370  blfvalps  12374  bldisj  12390  xblss2ps  12393  xblss2  12394  xblm  12406  blssps  12416  blss  12417  metss2lem  12486  metss2  12487  bdxmet  12490  bdbl  12492  metrest  12495  xmetxpbl  12497  xmettxlem  12498  xmettx  12499  metcnp3  12500  metcnp2  12502  metcnpi  12504  metcnpi2  12505  txmetcnp  12507  qtopbas  12511  tgioo  12532  addcncntoplem  12537  fsumcncntop  12542  rescncf  12554  cncfco  12564  cncfcncntop  12566  cncfmptid  12569  addccncf  12572  cdivcncfap  12573  negcncf  12574  mulcncflem  12576  mulcncf  12577  limccl  12584  ellimc3apf  12585  limcdifap  12587  limcmpted  12588  limcimolemlt  12589  limcimo  12590  cnplimcim  12592  cnplimclemle  12593  cnplimclemr  12594  cnlimcim  12596  limccnpcntop  12600  reldvg  12603  dvfvalap  12605  dvfgg  12612  dvidlemap  12615  dvcnp2cntop  12618  bj-nnan  12641  bj-indind  12822  bj-omtrans  12846  pwtrufal  12884  pwle2  12885  pwf1oexmid  12886  subctctexmid  12888  nnsf  12891  peano4nninf  12892  nninfalllemn  12894  nninfalllem1  12895  nninfall  12896  nninfself  12901  nninfsellemeq  12902  nninfsellemqall  12903  nninfsellemeqinf  12904  nninfsel  12905  nninfomnilem  12906  nninffeq  12908  sbthom  12913  qdencn  12914  refeq  12915  isomninnlem  12917  trilpolemclim  12921  trilpolemcl  12922  trilpolemisumle  12923  trilpolemeq1  12925  trilpolemlt1  12926  trilpolemres  12927