Theorem simplr 528

Description: Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)

Assertion

Ref	Expression
simplr	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

Proof of Theorem simplr

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad2antlr 489	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp1lr  1066  simp2lr  1070  simp3lr  1074  bilukdc  1418  dcun  3581  ifnefals  3627  intab  3931  exmid01  4261  exmidundif  4269  exmidundifim  4270  frirrg  4418  reg2exmidlema  4603  imadiflem  5376  fvco4  5679  fvmptt  5699  fcoconst  5779  funopsn  5790  f1imass  5871  fcof1  5880  fliftfun  5893  riotass2  5956  ovmpodxf  6101  dftpos4  6379  tfrlem1  6424  tfrlem3ag  6425  tfrlemibacc  6442  tfrlemibfn  6444  tfrlemi1  6448  tfrlemi14d  6449  tfr1onlem3ag  6453  tfr1onlembacc  6458  tfr1onlembfn  6460  tfr1onlemaccex  6464  tfrcllembacc  6471  tfrcllembfn  6473  tfrcllemaccex  6477  frecabcl  6515  nntr2  6619  dcdifsnid  6620  nnm00  6646  ecopovsymg  6751  ecopoverg  6753  th3qlem1  6754  mapss  6808  f1imaen2g  6915  pw2f1odclem  6963  xpen  6974  xpmapenlem  6978  phpm  6995  fidifsnen  7000  dif1enen  7010  fiunsnnn  7011  fin0  7015  fin0or  7016  findcard2d  7021  findcard2sd  7022  diffifi  7024  isinfinf  7027  tridc  7029  fimax2gtrilemstep  7030  fimax2gtri  7031  en2eqpr  7037  onunsnss  7047  unsnfidcex  7050  unsnfidcel  7051  undifdcss  7053  unfiin  7056  fisseneq  7064  ssfirab  7066  f1finf1o  7082  fidcenumlemrks  7088  fidcenumlemrk  7089  fidcenumlemr  7090  fidcenum  7091  suplub2ti  7136  supisolem  7143  ordiso2  7170  djudom  7228  omp1eomlem  7229  difinfsnlem  7234  difinfinf  7236  ctm  7244  ctssdclemn0  7245  enumct  7250  nnnninfeq  7263  nnnninfeq2  7264  nninfisol  7268  enomnilem  7273  finomni  7275  exmidomni  7277  fodju0  7282  ismkvnex  7290  enmkvlem  7296  enwomnilem  7304  pr2cv1  7336  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  exmidaclem  7358  exmidontriimlem1  7371  exmidontriimlem2  7372  exmidontriimlem3  7373  exmidontriimlem4  7374  exmidontriim  7375  netap  7408  exmidapne  7414  dfplpq2  7509  dfmpq2  7510  mulpipqqs  7528  nqpi  7533  distrnqg  7542  prarloclemarch  7573  enq0tr  7589  nqnq0pi  7593  nq0nn  7597  nnnq0lem1  7601  prarloclemup  7650  prarloclem3  7652  prarloclemcalc  7657  genplt2i  7665  addnqprllem  7682  addnqprulem  7683  appdivnq  7718  distrlem1prl  7737  distrlem1pru  7738  ltaddpr  7752  ltexprlemlol  7757  ltexprlemupu  7759  ltexprlemdisj  7761  addcanprleml  7769  ltaprlem  7773  addextpr  7776  recexprlemopu  7782  recexprlemdisj  7785  recexprlem1ssl  7788  aptiprleml  7794  cauappcvgprlemm  7800  cauappcvgprlemopl  7801  cauappcvgprlemlol  7802  cauappcvgprlemopu  7803  cauappcvgprlemdisj  7806  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  cauappcvgprlemladdru  7811  cauappcvgprlemladdrl  7812  caucvgprlemm  7823  caucvgprlemopl  7824  caucvgprlemlol  7825  caucvgprlemopu  7826  caucvgprlemladdfu  7832  caucvgprprlemml  7849  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemopu  7854  caucvgprprlemexbt  7861  suplocexprlemru  7874  suplocexprlemloc  7876  suplocexprlemub  7878  suplocexprlemlub  7879  prsrlem1  7897  recexgt0sr  7928  mulgt0sr  7933  archsr  7937  caucvgsrlemcau  7948  caucvgsrlemoffcau  7953  caucvgsrlemoffres  7955  suplocsrlemb  7961  suplocsrlempr  7962  suplocsrlem  7963  addcnsr  7989  mulcnsr  7990  mulcnsrec  7998  axmulcom  8026  nntopi  8049  axcaucvglemcau  8053  axcaucvglemres  8054  axpre-suploclemres  8056  axpre-suploc  8057  mpomulf  8104  axsuploc  8187  ltntri  8242  cnegexlem2  8290  cnegexlem3  8291  addsub4  8357  le2add  8559  lt2add  8560  lt2sub  8575  le2sub  8576  rereim  8701  apreim  8718  mulreim  8719  apcotr  8722  apadd1  8723  addext  8725  mulext1  8727  mulext  8729  apti  8737  aptap  8765  receuap  8784  rec11rap  8826  divdivdivap  8828  divadddivap  8842  divsubdivap  8843  rerecclap  8845  recgt0  8965  prodgt0gt0  8966  prodgt0  8967  prodge0  8969  lemulge11  8981  lt2mul2div  8994  ltrec  8998  lerec  8999  ltrec1  9003  lediv2a  9010  mulle0r  9059  sup3exmid  9072  zdiv  9503  eluzuzle  9698  supinfneg  9758  infsupneg  9759  infregelbex  9761  xrltso  9960  xnn0dcle  9966  xnn0letri  9967  npnflt  9979  nmnfgt  9982  z2ge  9990  xaddf  10008  xaddval  10009  xpncan  10035  xleadd1a  10037  xltadd1  10040  xaddge0  10042  xle2add  10043  xleaddadd  10051  ixxss1  10068  ixxss2  10069  elico2  10101  iccsupr  10130  fzass4  10226  fzrev  10248  fz0fzelfz0  10291  fzocatel  10372  elfzomelpfzo  10404  zsupcllemstep  10416  exbtwnzlemstep  10434  rebtwn2zlemstep  10439  qbtwnxr  10444  xqltnle  10454  apbtwnz  10461  btwnzge0  10487  modqid  10538  modqcyc  10548  modqcyc2  10549  modqaddabs  10551  modqaddmod  10552  mulqaddmodid  10553  modqmuladd  10555  modqltm1p1mod  10565  modqsubmod  10571  modqsubmodmod  10572  modaddmodlo  10577  modqmulmod  10578  modqmulmodr  10579  modqsubdir  10582  addmodlteq  10587  nninfinf  10632  iseqf1olemab  10691  iseqf1olemmo  10694  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  seqf1oglem1  10708  seqf1oglem2  10709  seqf1og  10710  exp3val  10730  expcl2lemap  10740  expap0  10758  expnegzap  10762  expmul  10773  leexp1a  10783  qsqeqor  10839  expnbnd  10852  nn0ltexp2  10898  nn0opth2  10913  facndiv  10928  faclbnd  10930  bcval5  10952  bcpasc  10955  hashennnuni  10968  hashunlem  10993  hashunsng  10996  hashprg  10997  fiprsshashgt1  11006  hashxp  11015  fimaxq  11016  zfz1isolemiso  11028  zfz1isolem1  11029  seq3coll  11031  iswrdiz  11045  wrdnval  11068  ccatlen  11096  ccatvalfn  11102  ccatsymb  11103  swrdclg  11148  swrdsb0eq  11163  pfxwrdsymbg  11188  wrdind  11220  wrd2ind  11221  swrdccatin2  11227  pfxccatin12lem2  11229  pfxccatin12  11231  pfxccat3  11232  swrdccat  11233  shftlem  11293  shftfvalg  11295  shftfval  11298  2shfti  11308  caucvgrelemrec  11456  caucvgrelemcau  11457  caucvgre  11458  cvg1nlemcau  11461  cvg1nlemres  11462  resqrexlemcalc3  11493  resqrexlemcvg  11496  resqrexlemglsq  11499  resqrexlemga  11500  sqrtsq  11521  leabs  11551  absexpzap  11557  abslt  11565  absle  11566  abssubap0  11567  caubnd2  11594  icodiamlt  11657  maxleim  11682  maxabslemval  11685  maxleastlt  11692  rexico  11698  zmaxcl  11701  fimaxre2  11704  minmax  11707  xrmaxleim  11721  xrmaxiflemcl  11722  xrmaxifle  11723  xrmaxiflemlub  11725  xrmaxiflemval  11727  xrmaxleastlt  11733  xrmaxltsup  11735  xrmaxadd  11738  xrminmax  11742  xrbdtri  11753  climuni  11770  climshftlemg  11779  iserex  11816  climcau  11824  climrecvg1n  11825  climcvg1nlem  11826  sumeq2  11836  summodclem3  11857  zsumdc  11861  isumss  11868  fisumss  11869  sumsnf  11886  fsumconst  11931  modfsummod  11935  fsum00  11939  fsumabs  11942  fsumrelem  11948  fsumiun  11954  isumsplit  11968  divcnv  11974  geo2sum  11991  geoisumr  11995  cvgratz  12009  ntrivcvgap  12025  prodeq2  12034  prodmodclem2  12054  prodmodc  12055  zproddc  12056  fprodmul  12068  prodsnf  12069  fprodcl2lem  12082  fprodconst  12097  fprodap0  12098  fprodrec  12106  fprodap0f  12113  fprodle  12117  fprodmodd  12118  tanaddap  12216  zdvdsdc  12289  dvds2ln  12301  fsumdvds  12319  dvdsle  12321  dvdsext  12332  divalglemeunn  12398  divalglemex  12399  divalglemeuneg  12400  bitsfzo  12432  bitsmod  12433  bitsinv1lem  12438  bitsinv1  12439  dvdsbnd  12443  gcdsupex  12444  gcdsupcl  12445  dvdslegcd  12451  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemmain  12485  bezoutlemzz  12489  bezoutlembz  12491  bezoutlembi  12492  bezoutlemle  12495  dfgcd3  12497  bezout  12498  dfgcd2  12501  dvdsmulgcd  12512  bezoutr  12519  uzwodc  12524  nninfctlemfo  12527  lcmval  12551  lcmcllem  12555  lcmneg  12562  ncoprmgcdne1b  12577  isprm2lem  12604  prmind2  12608  dvdsnprmd  12613  isprm5  12630  prmdvdsexp  12636  sqrt2irr  12650  oddpwdclemxy  12657  oddpwdclemdc  12661  nonsq  12695  pceu  12784  pcmul  12790  pc2dvds  12819  pcz  12821  pcprmpw2  12822  dvdsprmpweqle  12826  pcfac  12839  qexpz  12841  prmpwdvds  12844  1arith  12856  mul4sq  12883  4sqexercise2  12888  4sqlemsdc  12889  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemhom  12952  ennnfonelemfun  12954  ennnfonelemf1  12955  ennnfonelemim  12961  exmidunben  12963  ctiunctlemfo  12976  omiunct  12981  ssnnctlemct  12983  isstruct2r  13009  prdsval  13272  ismgm  13356  issgrp  13402  sgrppropd  13412  sgrpidmndm  13419  mndpropd  13439  issubmnd  13441  prdsidlem  13446  resmhm2b  13488  gsumwmhm  13497  isgrpinv  13553  grplmulf1o  13573  dfgrp3mlem  13597  grplactcnv  13601  pwssub  13612  mhmid  13618  mhmmnd  13619  ghmgrp  13621  mulgval  13625  mulgfng  13627  mulgnnp1  13633  mulgnn0dir  13655  mulgneg2  13659  mhmmulg  13666  grpissubg  13697  isnsg  13705  isnsg3  13710  nmzsubg  13713  ghmmhmb  13757  ghmpreima  13769  ghmnsgpreima  13772  ghmf1  13776  ghmf1o  13778  conjghm  13779  conjnmz  13782  conjnmzb  13783  ghmcmn  13830  gsumfzconst  13844  issrg  13894  srglmhm  13922  srgrmhm  13923  isring  13929  ringadd2  13956  ringlghm  13990  ringrghm  13991  oppr1g  14011  reldvdsrsrg  14021  dvdsrvald  14022  dvdsrd  14023  dvdsrex  14027  dvdsrmul1  14031  unitgrp  14045  rhmopp  14105  subrgintm  14172  subrgpropd  14182  isdomn  14198  lmodprop2d  14277  lssvacl  14294  lssvsubcl  14295  lssvscl  14304  lsslss  14310  lss1d  14312  lsspropdg  14360  expghmap  14536  mulgghm2  14537  znunit  14588  znrrg  14589  mplvalcoe  14619  mplsubgfilemcl  14628  mplsubgfileminv  14629  mplsubgfi  14630  opnssneib  14795  restbasg  14807  restopn2  14822  iscnp4  14857  cnss2  14866  cnconst2  14872  cnptopresti  14877  cnptoprest2  14879  neitx  14907  uptx  14913  txrest  14915  txdis1cn  14917  xmetres2  15018  xblss2ps  15043  blhalf  15047  blssps  15066  blss  15067  blssexps  15068  blssex  15069  blin2  15071  metequiv2  15135  bdmetval  15139  metcnp3  15150  metcnp  15151  metcn  15153  metcnpi  15154  metcnpi2  15155  txmetcnp  15157  txmetcn  15158  qtopbas  15161  tgqioo  15194  mpomulcn  15205  fsumcncntop  15206  elcncf2  15213  mulcncflem  15246  mulcncf  15247  suplociccreex  15263  limcdifap  15301  cnplimcim  15306  cnplimccntop  15309  limccnpcntop  15314  dvcj  15348  dvmptfsum  15364  dveflem  15365  ply1termlem  15381  plyaddlem1  15386  plymullem1  15387  plycolemc  15397  plycjlemc  15399  plyrecj  15402  dvply1  15404  reeff1olem  15410  eflt  15414  sin0pilem1  15420  ptolemy  15463  coseq0q4123  15473  coseq0negpitopi  15475  cos02pilt1  15490  cos11  15492  ioocosf1o  15493  rpcxpmul2  15552  cxplt  15555  cxple  15556  cxplt3  15559  apcxp2  15578  rprelogbmul  15594  rprelogbdiv  15596  dvdsppwf1o  15628  perfect  15640  lgsval  15648  lgsfcl2  15650  lgscllem  15651  lgsval2lem  15654  lgsdir2lem4  15675  lgsdir2lem5  15676  lgsdir2  15677  lgsne0  15682  gausslemma2dlem1a  15702  gausslemma2dlem1f1o  15704  2sqlem6  15764  2sqlem10  15769  umgrnloopv  15879  umgrvad2edg  15974  2omap  16270  pw1map  16272  pwle2  16275  pwf1oexmid  16276  subctctexmid  16277  pw1nct  16280  peano4nninf  16283  nninfalllem1  16285  nninfall  16286  nninfsellemeq  16291  nninfsellemqall  16292  nnnninfex  16299  nninfnfiinf  16300  sbthom  16305  refeq  16307  isomninnlem  16309  trilpolemeq1  16319  trilpolemlt1  16320  trirec0  16323  apdiff  16327  iswomninnlem  16328  ismkvnnlem  16331  redcwlpolemeq1  16333  ltlenmkv  16349