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  1085  simp2lr  1089  simp3lr  1093  bilukdc  1438  dcun  3602  ifnefals  3648  intab  3955  exmid01  4286  exmidundif  4294  exmidundifim  4295  frirrg  4445  reg2exmidlema  4630  imadiflem  5406  fvco4  5714  fvmptt  5734  fcoconst  5814  funopsn  5825  f1imass  5910  fcof1  5919  fliftfun  5932  riotass2  5995  ovmpodxf  6142  dftpos4  6424  tfrlem1  6469  tfrlem3ag  6470  tfrlemibacc  6487  tfrlemibfn  6489  tfrlemi1  6493  tfrlemi14d  6494  tfr1onlem3ag  6498  tfr1onlembacc  6503  tfr1onlembfn  6505  tfr1onlemaccex  6509  tfrcllembacc  6516  tfrcllembfn  6518  tfrcllemaccex  6522  frecabcl  6560  nntr2  6666  dcdifsnid  6667  nnm00  6693  ecopovsymg  6798  ecopoverg  6800  th3qlem1  6801  mapss  6855  f1imaen2g  6962  pw2f1odclem  7015  xpen  7026  xpmapenlem  7030  phpm  7047  fidifsnen  7052  dif1enen  7064  fiunsnnn  7065  fin0  7069  fin0or  7070  findcard2d  7075  findcard2sd  7076  diffifi  7078  isinfinf  7081  tridc  7084  fimax2gtrilemstep  7085  fimax2gtri  7086  en2eqpr  7094  onunsnss  7104  unsnfidcex  7107  unsnfidcel  7108  undifdcss  7110  unfiin  7113  fisseneq  7121  ssfirab  7123  f1finf1o  7140  fidcenumlemrks  7146  fidcenumlemrk  7147  fidcenumlemr  7148  fidcenum  7149  suplub2ti  7194  supisolem  7201  ordiso2  7228  djudom  7286  omp1eomlem  7287  difinfsnlem  7292  difinfinf  7294  ctm  7302  ctssdclemn0  7303  enumct  7308  nnnninfeq  7321  nnnninfeq2  7322  nninfisol  7326  enomnilem  7331  finomni  7333  exmidomni  7335  fodju0  7340  ismkvnex  7348  enmkvlem  7354  enwomnilem  7362  pr2cv1  7394  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  exmidaclem  7416  exmidontriimlem1  7429  exmidontriimlem2  7430  exmidontriimlem3  7431  exmidontriimlem4  7432  exmidontriim  7433  netap  7466  exmidapne  7472  dfplpq2  7567  dfmpq2  7568  mulpipqqs  7586  nqpi  7591  distrnqg  7600  prarloclemarch  7631  enq0tr  7647  nqnq0pi  7651  nq0nn  7655  nnnq0lem1  7659  prarloclemup  7708  prarloclem3  7710  prarloclemcalc  7715  genplt2i  7723  addnqprllem  7740  addnqprulem  7741  appdivnq  7776  distrlem1prl  7795  distrlem1pru  7796  ltaddpr  7810  ltexprlemlol  7815  ltexprlemupu  7817  ltexprlemdisj  7819  addcanprleml  7827  ltaprlem  7831  addextpr  7834  recexprlemopu  7840  recexprlemdisj  7843  recexprlem1ssl  7846  aptiprleml  7852  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemlol  7860  cauappcvgprlemopu  7861  cauappcvgprlemdisj  7864  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemopu  7884  caucvgprlemladdfu  7890  caucvgprprlemml  7907  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemopu  7912  caucvgprprlemexbt  7919  suplocexprlemru  7932  suplocexprlemloc  7934  suplocexprlemub  7936  suplocexprlemlub  7937  prsrlem1  7955  recexgt0sr  7986  mulgt0sr  7991  archsr  7995  caucvgsrlemcau  8006  caucvgsrlemoffcau  8011  caucvgsrlemoffres  8013  suplocsrlemb  8019  suplocsrlempr  8020  suplocsrlem  8021  addcnsr  8047  mulcnsr  8048  mulcnsrec  8056  axmulcom  8084  nntopi  8107  axcaucvglemcau  8111  axcaucvglemres  8112  axpre-suploclemres  8114  axpre-suploc  8115  mpomulf  8162  axsuploc  8245  ltntri  8300  cnegexlem2  8348  cnegexlem3  8349  addsub4  8415  le2add  8617  lt2add  8618  lt2sub  8633  le2sub  8634  rereim  8759  apreim  8776  mulreim  8777  apcotr  8780  apadd1  8781  addext  8783  mulext1  8785  mulext  8787  apti  8795  aptap  8823  receuap  8842  rec11rap  8884  divdivdivap  8886  divadddivap  8900  divsubdivap  8901  rerecclap  8903  recgt0  9023  prodgt0gt0  9024  prodgt0  9025  prodge0  9027  lemulge11  9039  lt2mul2div  9052  ltrec  9056  lerec  9057  ltrec1  9061  lediv2a  9068  mulle0r  9117  sup3exmid  9130  zdiv  9561  eluzuzle  9757  supinfneg  9822  infsupneg  9823  infregelbex  9825  xrltso  10024  xnn0dcle  10030  xnn0letri  10031  npnflt  10043  nmnfgt  10046  z2ge  10054  xaddf  10072  xaddval  10073  xpncan  10099  xleadd1a  10101  xltadd1  10104  xaddge0  10106  xle2add  10107  xleaddadd  10115  ixxss1  10132  ixxss2  10133  elico2  10165  iccsupr  10194  fzass4  10290  fzrev  10312  fz0fzelfz0  10355  fzocatel  10437  elfzomelpfzo  10469  zsupcllemstep  10482  exbtwnzlemstep  10500  rebtwn2zlemstep  10505  qbtwnxr  10510  xqltnle  10520  apbtwnz  10527  btwnzge0  10553  modqid  10604  modqcyc  10614  modqcyc2  10615  modqaddabs  10617  modqaddmod  10618  mulqaddmodid  10619  modqmuladd  10621  modqltm1p1mod  10631  modqsubmod  10637  modqsubmodmod  10638  modaddmodlo  10643  modqmulmod  10644  modqmulmodr  10645  modqsubdir  10648  addmodlteq  10653  nninfinf  10698  iseqf1olemab  10757  iseqf1olemmo  10760  iseqf1olemjpcl  10763  iseqf1olemqpcl  10764  seqf1oglem1  10774  seqf1oglem2  10775  seqf1og  10776  exp3val  10796  expcl2lemap  10806  expap0  10824  expnegzap  10828  expmul  10839  leexp1a  10849  qsqeqor  10905  expnbnd  10918  nn0ltexp2  10964  nn0opth2  10979  facndiv  10994  faclbnd  10996  bcval5  11018  bcpasc  11021  hashennnuni  11034  hashunlem  11060  hashunsng  11064  hashprg  11065  fiprsshashgt1  11074  hashxp  11083  fimaxq  11084  zfz1isolemiso  11096  zfz1isolem1  11097  seq3coll  11099  iswrdiz  11113  wrdnval  11137  ccatlen  11165  ccatvalfn  11171  ccatsymb  11172  ccatalpha  11183  ccat2s1fstg  11218  swrdclg  11224  swrdsb0eq  11239  pfxwrdsymbg  11264  wrdind  11296  wrd2ind  11297  swrdccatin2  11303  pfxccatin12lem2  11305  pfxccatin12  11307  pfxccat3  11308  swrdccat  11309  shftlem  11370  shftfvalg  11372  shftfval  11375  2shfti  11385  caucvgrelemrec  11533  caucvgrelemcau  11534  caucvgre  11535  cvg1nlemcau  11538  cvg1nlemres  11539  resqrexlemcalc3  11570  resqrexlemcvg  11573  resqrexlemglsq  11576  resqrexlemga  11577  sqrtsq  11598  leabs  11628  absexpzap  11634  abslt  11642  absle  11643  abssubap0  11644  caubnd2  11671  icodiamlt  11734  maxleim  11759  maxabslemval  11762  maxleastlt  11769  rexico  11775  zmaxcl  11778  fimaxre2  11781  minmax  11784  xrmaxleim  11798  xrmaxiflemcl  11799  xrmaxifle  11800  xrmaxiflemlub  11802  xrmaxiflemval  11804  xrmaxleastlt  11810  xrmaxltsup  11812  xrmaxadd  11815  xrminmax  11819  xrbdtri  11830  climuni  11847  climshftlemg  11856  iserex  11893  climcau  11901  climrecvg1n  11902  climcvg1nlem  11903  sumeq2  11913  summodclem3  11934  zsumdc  11938  isumss  11945  fisumss  11946  sumsnf  11963  fsumconst  12008  modfsummod  12012  fsum00  12016  fsumabs  12019  fsumrelem  12025  fsumiun  12031  isumsplit  12045  divcnv  12051  geo2sum  12068  geoisumr  12072  cvgratz  12086  ntrivcvgap  12102  prodeq2  12111  prodmodclem2  12131  prodmodc  12132  zproddc  12133  fprodmul  12145  prodsnf  12146  fprodcl2lem  12159  fprodconst  12174  fprodap0  12175  fprodrec  12183  fprodap0f  12190  fprodle  12194  fprodmodd  12195  tanaddap  12293  zdvdsdc  12366  dvds2ln  12378  fsumdvds  12396  dvdsle  12398  dvdsext  12409  divalglemeunn  12475  divalglemex  12476  divalglemeuneg  12477  bitsfzo  12509  bitsmod  12510  bitsinv1lem  12515  bitsinv1  12516  dvdsbnd  12520  gcdsupex  12521  gcdsupcl  12522  dvdslegcd  12528  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlemzz  12566  bezoutlembz  12568  bezoutlembi  12569  bezoutlemle  12572  dfgcd3  12574  bezout  12575  dfgcd2  12578  dvdsmulgcd  12589  bezoutr  12596  uzwodc  12601  nninfctlemfo  12604  lcmval  12628  lcmcllem  12632  lcmneg  12639  ncoprmgcdne1b  12654  isprm2lem  12681  prmind2  12685  dvdsnprmd  12690  isprm5  12707  prmdvdsexp  12713  sqrt2irr  12727  oddpwdclemxy  12734  oddpwdclemdc  12738  nonsq  12772  pceu  12861  pcmul  12867  pc2dvds  12896  pcz  12898  pcprmpw2  12899  dvdsprmpweqle  12903  pcfac  12916  qexpz  12918  prmpwdvds  12921  1arith  12933  mul4sq  12960  4sqexercise2  12965  4sqlemsdc  12966  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemhom  13029  ennnfonelemfun  13031  ennnfonelemf1  13032  ennnfonelemim  13038  exmidunben  13040  ctiunctlemfo  13053  omiunct  13058  ssnnctlemct  13060  isstruct2r  13086  prdsval  13349  ismgm  13433  issgrp  13479  sgrppropd  13489  sgrpidmndm  13496  mndpropd  13516  issubmnd  13518  prdsidlem  13523  resmhm2b  13565  gsumwmhm  13574  isgrpinv  13630  grplmulf1o  13650  dfgrp3mlem  13674  grplactcnv  13678  pwssub  13689  mhmid  13695  mhmmnd  13696  ghmgrp  13698  mulgval  13702  mulgfng  13704  mulgnnp1  13710  mulgnn0dir  13732  mulgneg2  13736  mhmmulg  13743  grpissubg  13774  isnsg  13782  isnsg3  13787  nmzsubg  13790  ghmmhmb  13834  ghmpreima  13846  ghmnsgpreima  13849  ghmf1  13853  ghmf1o  13855  conjghm  13856  conjnmz  13859  conjnmzb  13860  ghmcmn  13907  gsumfzconst  13921  issrg  13971  srglmhm  13999  srgrmhm  14000  isring  14006  ringadd2  14033  ringlghm  14067  ringrghm  14068  oppr1g  14088  dvdsrvald  14100  dvdsrd  14101  dvdsrex  14105  dvdsrmul1  14109  unitgrp  14123  rhmopp  14183  subrgintm  14250  subrgpropd  14260  isdomn  14276  lmodprop2d  14355  lssvacl  14372  lssvsubcl  14373  lssvscl  14382  lsslss  14388  lss1d  14390  lsspropdg  14438  expghmap  14614  mulgghm2  14615  znunit  14666  znrrg  14667  mplvalcoe  14697  mplsubgfilemcl  14706  mplsubgfileminv  14707  mplsubgfi  14708  opnssneib  14873  restbasg  14885  restopn2  14900  iscnp4  14935  cnss2  14944  cnconst2  14950  cnptopresti  14955  cnptoprest2  14957  neitx  14985  uptx  14991  txrest  14993  txdis1cn  14995  xmetres2  15096  xblss2ps  15121  blhalf  15125  blssps  15144  blss  15145  blssexps  15146  blssex  15147  blin2  15149  metequiv2  15213  bdmetval  15217  metcnp3  15228  metcnp  15229  metcn  15231  metcnpi  15232  metcnpi2  15233  txmetcnp  15235  txmetcn  15236  qtopbas  15239  tgqioo  15272  mpomulcn  15283  fsumcncntop  15284  elcncf2  15291  mulcncflem  15324  mulcncf  15325  suplociccreex  15341  limcdifap  15379  cnplimcim  15384  cnplimccntop  15387  limccnpcntop  15392  dvcj  15426  dvmptfsum  15442  dveflem  15443  ply1termlem  15459  plyaddlem1  15464  plymullem1  15465  plycolemc  15475  plycjlemc  15477  plyrecj  15480  dvply1  15482  reeff1olem  15488  eflt  15492  sin0pilem1  15498  ptolemy  15541  coseq0q4123  15551  coseq0negpitopi  15553  cos02pilt1  15568  cos11  15570  ioocosf1o  15571  rpcxpmul2  15630  cxplt  15633  cxple  15634  cxplt3  15637  apcxp2  15656  rprelogbmul  15672  rprelogbdiv  15674  dvdsppwf1o  15706  perfect  15718  lgsval  15726  lgsfcl2  15728  lgscllem  15729  lgsval2lem  15732  lgsdir2lem4  15753  lgsdir2lem5  15754  lgsdir2  15755  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  2sqlem6  15842  2sqlem10  15847  umgrnloopv  15958  umgrvad2edg  16055  usgr1eop  16089  wlkvtxiedg  16156  wlkvtxiedgg  16157  upgredginwlk  16167  upgriswlkdc  16171  clwwlkccatlem  16209  pw1ndom3  16539  2omap  16544  pw1map  16546  pwle2  16549  pwf1oexmid  16550  subctctexmid  16551  pw1nct  16554  peano4nninf  16558  nninfalllem1  16560  nninfall  16561  nninfsellemeq  16566  nninfsellemqall  16567  nnnninfex  16574  nninfnfiinf  16575  sbthom  16580  refeq  16582  isomninnlem  16584  trilpolemeq1  16594  trilpolemlt1  16595  trirec0  16598  apdiff  16602  iswomninnlem  16603  ismkvnnlem  16606  redcwlpolemeq1  16608  ltlenmkv  16624