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

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

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  863  intnan  874  intnand  876  dcan  878  bimsc1  907  niabn  911  simp1r  966  simp2r  968  simp3r  970  3anandirs  1282  bilukdc  1330  19.26  1413  exsimpr  1552  19.40  1565  cbvexh  1682  sbequilem  1763  spsbe  1767  cbvexdh  1846  euan  2001  moan  2014  datisi  2055  fresison  2063  rexex  2418  r19.26  2493  r19.29an  2506  r19.40  2517  cbvraldva2  2590  cbvrexdva2  2591  gencbvex  2659  rspct  2708  rspcimdv  2716  rspcimedv  2717  rr19.28v  2747  elrab3t  2761  reu6  2795  rmob  2920  csbiebt  2956  rabssab  3097  ssddif  3222  difin  3225  difrab  3262  eqifdc  3411  ifmdc  3414  preqsn  3604  opprc2  3630  dfnfc2  3656  intmin4  3701  sndisj  3818  undifexmid  4004  exmid01  4008  exmidundif  4011  exss  4030  euotd  4057  frirrg  4153  suctr  4224  ordtri2or2exmid  4362  wetriext  4367  reg3exmidlemwe  4369  tfisi  4377  peano2  4385  omsinds  4410  relop  4556  releldm  4640  relelrn  4641  resiexg  4726  trin2  4792  xpmlem  4820  unielrel  4926  relcoi2  4929  iota2df  4972  iota2  4974  funopab4  5018  fun11uni  5051  imadiflem  5060  imain  5063  fneq12  5074  f1ssr  5188  fvelrnb  5317  ssimaex  5330  fvmpt2d  5354  fvmptdf  5355  dffo3  5411  ffvresb  5426  fmptco  5429  funfvima3  5491  f1imass  5516  fliftf  5541  fliftval  5542  riota2df  5591  riota5f  5595  acexmidlemcase  5610  ovprc2  5645  eloprabga  5694  eqfnov2  5711  ovmpt2dxf  5729  fnofval  5824  offval2  5829  ofrfval2  5830  caofinvl  5836  2ndrn  5912  1st2ndbr  5913  cnvf1o  5949  f1o2ndf1  5952  mpt2xopoveq  5961  sprmpt2  5963  dftpos4  5984  tpostpos  5985  tposf12  5990  dfsmo2  6008  smores  6013  tfrlem1  6029  tfrlem3ag  6030  tfrlem3a  6031  tfrlemisucaccv  6046  tfrlemi1  6053  tfrexlem  6055  tfr1onlem3ag  6058  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfr1onlembfn  6065  tfr1onlemaccex  6069  tfr1onlemres  6070  tfri1dALT  6072  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllembfn  6078  tfrcllemaccex  6082  tfrcllemres  6083  tfrcl  6085  rdgivallem  6102  rdgon  6107  frecabex  6119  frecabcl  6120  frectfr  6121  frecrdg  6129  oawordi  6186  nntri3  6214  dcdifsnid  6219  nnaordi  6221  nnaordex  6240  nnawordex  6241  nnm00  6242  ersymb  6260  ertr  6261  erref  6266  iserd  6272  swoer  6274  erth  6290  iinerm  6318  erinxp  6320  ecinxp  6321  qsel  6323  qliftel  6326  qliftfun  6328  fvdiagfn  6404  dom3  6447  ssdomg  6449  cnven  6479  xpen  6515  xpmapenlem  6519  ssenen  6521  phplem4dom  6532  phpm  6535  phpelm  6536  fidifsnen  6540  fin0  6555  fin0or  6556  isinfinf  6567  tridc  6569  fimax2gtrilemstep  6570  fimax2gtri  6571  finexdc  6572  en2eqpr  6577  fientri3  6579  unsnfidcex  6584  unsnfidcel  6585  unfidisj  6586  undifdcss  6587  undifdc  6588  unfiin  6590  fnfi  6599  relcnvfi  6603  f1dmvrnfibi  6606  f1finf1o  6608  suplubti  6642  suplub2ti  6643  supelti  6644  supisolem  6650  supisoex  6651  infglbti  6667  ordiso2  6675  djuss  6708  updjudhcoinlf  6718  updjudhcoinrg  6719  updjud  6720  djudom  6734  enomnilem  6741  finomni  6743  exmidomni  6745  fodjuomnilemdc  6746  fodjuomnilemres  6750  nnnninf  6753  en2eleq  6768  en2other2  6769  exmidfodomrlemeldju  6772  exmidfodomrlemreseldju  6773  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  dmaddpqlem  6883  nqpi  6884  mulcanenq  6891  ltaddnq  6913  ltexnqq  6914  prarloclemarch2  6925  ltrnqg  6926  ltnnnq  6929  enq0sym  6938  nqnq0pi  6944  nq0nn  6948  mulcanenq0ec  6951  addnq0mo  6953  mulnq0mo  6954  addnnnq0  6955  prloc  6997  prarloclemlt  6999  prarloclemlo  7000  ltdfpr  7012  genplt2i  7016  genpml  7023  genpmu  7024  addnqprllem  7033  addnqprulem  7034  addnqprl  7035  addnqpru  7036  nqprloc  7051  appdivnq  7069  appdiv0nq  7070  mulnqprl  7074  mulnqpru  7075  distrlem1prl  7088  distrlem1pru  7089  ltprordil  7095  1idprl  7096  1idpru  7097  ltexprlemrl  7116  ltexprlemru  7118  ltexpri  7119  addcanprleml  7120  addcanprlemu  7121  recexprlem1ssl  7139  recexpr  7144  aptiprlemu  7146  archpr  7149  cauappcvgprlemopl  7152  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgprlemm  7174  caucvgprlemopl  7175  caucvgprlemloc  7181  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlemlim  7187  caucvgprprlemval  7194  caucvgprprlemml  7200  caucvgprprlemopl  7203  caucvgprprlemopu  7205  caucvgprprlemloc  7209  caucvgprprlemexbt  7212  caucvgprprlemexb  7213  caucvgprprlemaddq  7214  caucvgprprlemlim  7217  addsrmo  7236  mulsrmo  7237  addsrpr  7238  mulsrpr  7239  0idsr  7260  1idsr  7261  recexsrlem  7267  addgt0sr  7268  srpospr  7275  prsradd  7278  prsrlt  7279  caucvgsrlemfv  7283  caucvgsrlemgt1  7287  caucvgsrlemoffval  7288  caucvgsrlemoffcau  7290  caucvgsrlemoffres  7292  rereceu  7371  axarch  7373  nntopi  7376  axcaucvglemval  7379  muladd11r  7585  cnegexlem1  7604  cnegex  7607  negeu  7620  pncan  7635  pncan3  7637  npcan  7638  addid0  7798  negf1o  7807  mulneg1  7820  lelttrdi  7851  ltnegcon2  7889  add20  7899  subge0  7900  lesub0  7904  reapval  7997  recexre  7999  apreap  8008  ltmul1a  8012  reapneg  8018  cru  8023  apsym  8027  apcotr  8028  apadd1  8029  apneg  8032  mulext1  8033  apti  8043  gt0ap0  8046  ap0gt0  8059  recexap  8064  divmulassap  8104  divmulasscomap  8105  rerecclap  8139  recgt0  8249  prodgt0gt0  8250  lemul1a  8257  lemul12a  8261  lt2msq  8285  ltrec1  8287  recreclt  8299  negiso  8354  creui  8358  cju  8359  avglt2  8591  un0addcl  8642  nn0ge2m1nn  8669  nn0nndivcl  8671  elnn0z  8699  peano2z  8722  elz2  8754  suprzclex  8780  peano5uzti  8790  zindd  8800  eluzadd  8982  nn0pzuz  9010  supinfneg  9018  infsupneg  9019  eluz2b2  9025  eqreznegel  9034  nn0ge2m1nnALT  9038  divfnzn  9041  qmulz  9043  qapne  9059  qreccl  9062  cnref1o  9068  ge0p1rp  9100  xrltso  9201  z2ge  9223  xltnegi  9232  ixxssixx  9255  lincmb01cmp  9355  iccf1o  9356  zltaddlt1le  9358  fztri3or  9388  fzdcel  9389  fznlem  9390  fzn  9391  uzsubsubfz  9396  fzsplit2  9399  fzopth  9409  fzdifsuc  9428  fzrev2i  9433  elfz1b  9437  fzneuz  9448  fzrevral  9452  ige2m1fz  9457  elfz0ubfz0  9467  elfz0fzfz0  9468  4fvwrd4  9482  2ffzeq  9483  fzospliti  9518  fzosplit  9519  fzo1fzo0n0  9525  fzonmapblen  9529  fzoaddel  9534  fzosubel  9536  fzosubel3  9538  elfzodifsumelfzo  9543  elfzom1elp1fzo  9544  elfzom1p1elfzo  9556  elfzonelfzo  9572  peano2fzor  9574  exfzdc  9582  fvinim0ffz  9583  qtri3or  9585  exbtwnzlemstep  9590  rebtwn2zlemstep  9595  qbtwnxr  9600  apbtwnz  9612  flqge  9620  flqltnz  9625  flqaddz  9635  btwnzge0  9638  flltdivnn0lt  9642  intfracq  9658  flqdiv  9659  modqid0  9688  q0mod  9693  q1mod  9694  modqmuladdim  9705  modqmuladdnn0  9706  q2txmodxeq0  9722  q2submod  9723  modifeq2int  9724  modqsubdir  9731  modsumfzodifsn  9734  addmodlteq  9736  frec2uzzd  9738  frec2uzuzd  9740  frec2uzrand  9743  frec2uzf1od  9744  frecuzrdgrrn  9746  frec2uzrdg  9747  frecuzrdgtcl  9750  frecuzrdgsuc  9752  frecuzrdgg  9754  frecuzrdgdomlem  9755  frecuzrdgfunlem  9757  frecuzrdgsuctlem  9761  frecfzennn  9764  uzsinds  9779  iseqvalt  9793  iseqclt  9801  iseqoveq  9802  iseqss  9803  iseqsst  9804  iseqfeq2  9807  iseqfeq  9809  isermono  9815  iseqsplit  9816  iseqf1olemkle  9821  iseqf1olemklt  9822  iseqf1olemqcl  9823  iseqf1olemnab  9825  iseqf1olemab  9826  iseqf1olemqf  9828  iseqf1olemmo  9829  iseqf1olemqf1o  9830  iseqf1olemqk  9831  iseqf1olemjpcl  9832  iseqf1olemqpcl  9833  iseqf1olemfvp  9834  iseqf1olemqsumkj  9835  iseqf1olemqsumk  9836  iseqf1olemqsum  9837  iseqf1oleml  9840  iseqf1o  9841  iseqid3s  9845  iseqid  9846  iseqhomo  9848  iseqz  9849  fser0const  9853  expivallem  9858  expival  9859  expinnval  9860  expp1  9864  rpexpcl  9876  expaddzaplem  9900  leexp1a  9912  exple1  9913  subsq  9962  binom2  9966  binom3  9971  bernneq3  9976  expnbnd  9977  expcan  10025  nn0opthd  10030  faclbnd  10049  faclbnd6  10052  facubnd  10053  facavg  10054  bcval  10057  bccmpl  10062  ibcval5  10071  bcpasc  10074  hashennnuni  10087  hashennn  10088  hashfiv01gt1  10090  fihasheqf1oi  10096  hashnncl  10104  fseq1hash  10109  fiprsshashgt1  10125  fimaxq  10135  fnfz0hash  10137  ffzo0hash  10139  zfz1isolemiso  10144  zfz1iso  10146  iseqcoll  10147  shftfvalg  10152  ovshftex  10153  shftdm  10156  shftfib  10157  shftval  10159  shftval5  10163  shftf  10164  2shfti  10165  crre  10190  rereb  10196  cjreim2  10237  cjap  10239  caucvgrelemrec  10311  caucvgrelemcau  10312  caucvgre  10313  cvg1nlemf  10315  cvg1nlemres  10317  uzin2  10319  rexuz3  10322  recvguniq  10327  sqrt0  10336  resqrexlemdecn  10344  resqrexlemlo  10345  resqrexlemcalc3  10348  resqrexlemnm  10350  resqrexlemcvg  10351  resqrexlemoverl  10353  resqrexlemglsq  10354  resqrexlemga  10355  resqrex  10358  sqrtgt0  10366  absrpclap  10393  absext  10395  absmul  10401  leabs  10406  nn0abscl  10417  ltabs  10419  abslt  10420  absle  10421  abssubap0  10422  abstri  10436  cau3lem  10446  caubnd2  10449  maxabsle  10536  maxabslemlub  10539  maxabslemval  10540  maxcl  10542  maxleastb  10546  maxltsup  10550  rexanre  10552  rexico  10553  zmaxcl  10555  fimaxre2  10556  minmax  10559  min2inf  10561  clim  10567  climi2  10574  climconst2  10577  climuni  10579  climmpt  10586  climshftlemg  10588  climres  10589  climcn1  10594  subcn2  10597  cn1lem  10599  climadd  10611  climmul  10612  climsub  10613  climle  10619  climsqz  10620  climsqz2  10621  clim2iser  10622  clim2iser2  10623  iiserex  10624  iisermulc2  10625  iserile  10627  iserige0  10628  climub  10629  climserile  10630  climrecvg1n  10632  climcvg1nlem  10633  serif0  10636  sumeq2  10643  sumfct  10658  isumrblem  10660  fisumcvg  10661  isumrb  10662  isummolem2a  10665  isummolem2  10666  isummo  10667  zisum  10668  iisum  10669  fisum  10670  sum0  10671  isumz  10672  fsumf1o  10673  isumss  10674  fisumss  10675  isumss2  10676  fisumcvg2  10677  fisumcvg3  10679  fsumcl2lem  10680  fsumcllem  10681  fsumadd  10688  fsumsplit  10689  sumsnf  10691  dvdsval2  10705  dvdsdc  10710  moddvds  10711  zdvdsdc  10723  dvdscmul  10729  dvdsmulc  10730  dvdscmulr  10731  dvdsmulcr  10732  modmulconst  10734  dvdsadd  10745  dvdsadd2b  10749  dvdslelemd  10750  dvdsle  10751  dvdsabseq  10754  dvdseq  10755  divconjdvds  10756  dvds1  10760  fzo0dvdseq  10764  dvdsmod  10769  oddm1even  10781  mod2eq1n2dvds  10785  evennn02n  10788  evennn2n  10789  divalglemnn  10824  divalglemnqt  10826  divalglemeunn  10827  divalglemex  10828  divalglemeuneg  10829  divalg  10830  divalgmod  10833  modremain  10835  infssuzex  10851  gcdsupex  10855  gcdsupcl  10856  gcdval  10857  dvdslegcd  10862  gcdnncl  10865  gcdneg  10879  gcdaddm  10881  gcd1  10884  bezoutlemnewy  10891  bezoutlemmain  10893  bezoutlemex  10896  bezoutlemzz  10897  bezoutlemaz  10898  bezoutlembz  10899  bezoutlembi  10900  bezoutlemle  10903  bezoutlemsup  10904  gcdass  10910  gcdzeq  10917  dvdsmulgcd  10920  bezoutr1  10928  ialgrp1  10934  ialgcvga  10939  eucalgval2  10941  eucalgf  10943  eucalglt  10945  lcmval  10951  lcmledvds  10958  lcmneg  10962  lcmgcd  10966  lcmid  10968  coprmgcdb  10976  ncoprmgcdne1b  10977  mulgcddvds  10982  rpmulgcd2  10983  qredeq  10984  divgcdcoprm0  10989  divgcdcoprmex  10990  cncongr1  10991  cncongr2  10992  isprm2lem  11004  prmind2  11008  sqnprm  11023  isprm6  11032  prmdvdsexp  11033  prmfac1  11037  rpexp  11038  rpexp1i  11039  sqrt2irr  11047  pw2dvdslemn  11049  pw2dvdseulemle  11051  oddpwdclemxy  11053  oddpwdclemdc  11057  oddpwdc  11058  znege1  11062  sqrt2irraplemnn  11063  sqrt2irrap  11064  divnumden  11080  qden1elz  11089  phibndlem  11098  dfphi2  11102  phiprmpw  11104  crth  11106  phimullem  11107  oddennn  11111  evenennn  11112  bj-indind  11296  bj-omtrans  11320  nnpredcl  11359  nnsf  11364  peano4nninf  11365  nninfalllemn  11367  nninfalllem1  11368  nninfall  11369  nninfself  11374  nninfsellemeq  11375  nninfsellemqall  11376  nninfsellemeqinf  11377  nninfsel  11378  nninfomnilem  11379  qdencn  11384