Theorem simplr 529

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  1087  simp2lr  1091  simp3lr  1095  bilukdc  1440  dcun  3603  ifnefals  3651  intab  3958  exmid01  4290  exmidundif  4298  exmidundifim  4299  frirrg  4449  reg2exmidlema  4634  imadiflem  5411  fvco4  5721  fvmptt  5741  fcoconst  5821  funopsn  5833  f1imass  5920  fcof1  5929  fliftfun  5942  riotass2  6005  ovmpodxf  6152  dftpos4  6434  tfrlem1  6479  tfrlem3ag  6480  tfrlemibacc  6497  tfrlemibfn  6499  tfrlemi1  6503  tfrlemi14d  6504  tfr1onlem3ag  6508  tfr1onlembacc  6513  tfr1onlembfn  6515  tfr1onlemaccex  6519  tfrcllembacc  6526  tfrcllembfn  6528  tfrcllemaccex  6532  frecabcl  6570  nntr2  6676  dcdifsnid  6677  nnm00  6703  ecopovsymg  6808  ecopoverg  6810  th3qlem1  6811  mapss  6865  f1imaen2g  6972  pw2f1odclem  7025  xpen  7036  xpmapenlem  7040  phpm  7057  fidifsnen  7062  dif1enen  7074  fiunsnnn  7075  fin0  7079  fin0or  7080  findcard2d  7085  findcard2sd  7086  diffifi  7088  isinfinf  7091  tridc  7094  fimax2gtrilemstep  7095  fimax2gtri  7096  en2eqpr  7104  onunsnss  7114  unsnfidcex  7117  unsnfidcel  7118  undifdcss  7120  unfiin  7123  fisseneq  7132  ssfirab  7134  f1finf1o  7151  fidcenumlemrks  7157  fidcenumlemrk  7158  fidcenumlemr  7159  fidcenum  7160  suplub2ti  7205  supisolem  7212  ordiso2  7239  djudom  7297  omp1eomlem  7298  difinfsnlem  7303  difinfinf  7305  ctm  7313  ctssdclemn0  7314  enumct  7319  nnnninfeq  7332  nnnninfeq2  7333  nninfisol  7337  enomnilem  7342  finomni  7344  exmidomni  7346  fodju0  7351  ismkvnex  7359  enmkvlem  7365  enwomnilem  7373  pr2cv1  7405  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  exmidaclem  7428  exmidontriimlem1  7441  exmidontriimlem2  7442  exmidontriimlem3  7443  exmidontriimlem4  7444  exmidontriim  7445  netap  7478  exmidapne  7484  dfplpq2  7579  dfmpq2  7580  mulpipqqs  7598  nqpi  7603  distrnqg  7612  prarloclemarch  7643  enq0tr  7659  nqnq0pi  7663  nq0nn  7667  nnnq0lem1  7671  prarloclemup  7720  prarloclem3  7722  prarloclemcalc  7727  genplt2i  7735  addnqprllem  7752  addnqprulem  7753  appdivnq  7788  distrlem1prl  7807  distrlem1pru  7808  ltaddpr  7822  ltexprlemlol  7827  ltexprlemupu  7829  ltexprlemdisj  7831  addcanprleml  7839  ltaprlem  7843  addextpr  7846  recexprlemopu  7852  recexprlemdisj  7855  recexprlem1ssl  7858  aptiprleml  7864  cauappcvgprlemm  7870  cauappcvgprlemopl  7871  cauappcvgprlemlol  7872  cauappcvgprlemopu  7873  cauappcvgprlemdisj  7876  cauappcvgprlemladdfu  7879  cauappcvgprlemladdfl  7880  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  caucvgprlemm  7893  caucvgprlemopl  7894  caucvgprlemlol  7895  caucvgprlemopu  7896  caucvgprlemladdfu  7902  caucvgprprlemml  7919  caucvgprprlemopl  7922  caucvgprprlemlol  7923  caucvgprprlemopu  7924  caucvgprprlemexbt  7931  suplocexprlemru  7944  suplocexprlemloc  7946  suplocexprlemub  7948  suplocexprlemlub  7949  prsrlem1  7967  recexgt0sr  7998  mulgt0sr  8003  archsr  8007  caucvgsrlemcau  8018  caucvgsrlemoffcau  8023  caucvgsrlemoffres  8025  suplocsrlemb  8031  suplocsrlempr  8032  suplocsrlem  8033  addcnsr  8059  mulcnsr  8060  mulcnsrec  8068  axmulcom  8096  nntopi  8119  axcaucvglemcau  8123  axcaucvglemres  8124  axpre-suploclemres  8126  axpre-suploc  8127  mpomulf  8174  axsuploc  8257  ltntri  8312  cnegexlem2  8360  cnegexlem3  8361  addsub4  8427  le2add  8629  lt2add  8630  lt2sub  8645  le2sub  8646  rereim  8771  apreim  8788  mulreim  8789  apcotr  8792  apadd1  8793  addext  8795  mulext1  8797  mulext  8799  apti  8807  aptap  8835  receuap  8854  rec11rap  8896  divdivdivap  8898  divadddivap  8912  divsubdivap  8913  rerecclap  8915  recgt0  9035  prodgt0gt0  9036  prodgt0  9037  prodge0  9039  lemulge11  9051  lt2mul2div  9064  ltrec  9068  lerec  9069  ltrec1  9073  lediv2a  9080  mulle0r  9129  sup3exmid  9142  zdiv  9573  eluzuzle  9769  supinfneg  9834  infsupneg  9835  infregelbex  9837  xrltso  10036  xnn0dcle  10042  xnn0letri  10043  npnflt  10055  nmnfgt  10058  z2ge  10066  xaddf  10084  xaddval  10085  xpncan  10111  xleadd1a  10113  xltadd1  10116  xaddge0  10118  xle2add  10119  xleaddadd  10127  ixxss1  10144  ixxss2  10145  elico2  10177  iccsupr  10206  fzass4  10302  fzrev  10324  fz0fzelfz0  10367  fzocatel  10450  elfzomelpfzo  10482  zsupcllemstep  10495  exbtwnzlemstep  10513  rebtwn2zlemstep  10518  qbtwnxr  10523  xqltnle  10533  apbtwnz  10540  btwnzge0  10566  modqid  10617  modqcyc  10627  modqcyc2  10628  modqaddabs  10630  modqaddmod  10631  mulqaddmodid  10632  modqmuladd  10634  modqltm1p1mod  10644  modqsubmod  10650  modqsubmodmod  10651  modaddmodlo  10656  modqmulmod  10657  modqmulmodr  10658  modqsubdir  10661  addmodlteq  10666  nninfinf  10711  iseqf1olemab  10770  iseqf1olemmo  10773  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  seqf1oglem1  10787  seqf1oglem2  10788  seqf1og  10789  exp3val  10809  expcl2lemap  10819  expap0  10837  expnegzap  10841  expmul  10852  leexp1a  10862  qsqeqor  10918  expnbnd  10931  nn0ltexp2  10977  nn0opth2  10992  facndiv  11007  faclbnd  11009  bcval5  11031  bcpasc  11034  hashennnuni  11047  hashunlem  11073  hashunsng  11077  hashprg  11078  fiprsshashgt1  11087  hashxp  11096  fimaxq  11097  zfz1isolemiso  11109  zfz1isolem1  11110  seq3coll  11112  iswrdiz  11129  wrdnval  11153  ccatlen  11181  ccatvalfn  11187  ccatsymb  11188  ccatalpha  11199  ccat2s1fstg  11234  swrdclg  11240  swrdsb0eq  11255  pfxwrdsymbg  11280  wrdind  11312  wrd2ind  11313  swrdccatin2  11319  pfxccatin12lem2  11321  pfxccatin12  11323  pfxccat3  11324  swrdccat  11325  shftlem  11399  shftfvalg  11401  shftfval  11404  2shfti  11414  caucvgrelemrec  11562  caucvgrelemcau  11563  caucvgre  11564  cvg1nlemcau  11567  cvg1nlemres  11568  resqrexlemcalc3  11599  resqrexlemcvg  11602  resqrexlemglsq  11605  resqrexlemga  11606  sqrtsq  11627  leabs  11657  absexpzap  11663  abslt  11671  absle  11672  abssubap0  11673  caubnd2  11700  icodiamlt  11763  maxleim  11788  maxabslemval  11791  maxleastlt  11798  rexico  11804  zmaxcl  11807  fimaxre2  11810  minmax  11813  xrmaxleim  11827  xrmaxiflemcl  11828  xrmaxifle  11829  xrmaxiflemlub  11831  xrmaxiflemval  11833  xrmaxleastlt  11839  xrmaxltsup  11841  xrmaxadd  11844  xrminmax  11848  xrbdtri  11859  climuni  11876  climshftlemg  11885  iserex  11922  climcau  11930  climrecvg1n  11931  climcvg1nlem  11932  sumeq2  11942  summodclem3  11964  zsumdc  11968  isumss  11975  fisumss  11976  sumsnf  11993  fsumconst  12038  modfsummod  12042  fsum00  12046  fsumabs  12049  fsumrelem  12055  fsumiun  12061  isumsplit  12075  divcnv  12081  geo2sum  12098  geoisumr  12102  cvgratz  12116  ntrivcvgap  12132  prodeq2  12141  prodmodclem2  12161  prodmodc  12162  zproddc  12163  fprodmul  12175  prodsnf  12176  fprodcl2lem  12189  fprodconst  12204  fprodap0  12205  fprodrec  12213  fprodap0f  12220  fprodle  12224  fprodmodd  12225  tanaddap  12323  zdvdsdc  12396  dvds2ln  12408  fsumdvds  12426  dvdsle  12428  dvdsext  12439  divalglemeunn  12505  divalglemex  12506  divalglemeuneg  12507  bitsfzo  12539  bitsmod  12540  bitsinv1lem  12545  bitsinv1  12546  dvdsbnd  12550  gcdsupex  12551  gcdsupcl  12552  dvdslegcd  12558  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemmain  12592  bezoutlemzz  12596  bezoutlembz  12598  bezoutlembi  12599  bezoutlemle  12602  dfgcd3  12604  bezout  12605  dfgcd2  12608  dvdsmulgcd  12619  bezoutr  12626  uzwodc  12631  nninfctlemfo  12634  lcmval  12658  lcmcllem  12662  lcmneg  12669  ncoprmgcdne1b  12684  isprm2lem  12711  prmind2  12715  dvdsnprmd  12720  isprm5  12737  prmdvdsexp  12743  sqrt2irr  12757  oddpwdclemxy  12764  oddpwdclemdc  12768  nonsq  12802  pceu  12891  pcmul  12897  pc2dvds  12926  pcz  12928  pcprmpw2  12929  dvdsprmpweqle  12933  pcfac  12946  qexpz  12948  prmpwdvds  12951  1arith  12963  mul4sq  12990  4sqexercise2  12995  4sqlemsdc  12996  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemhom  13059  ennnfonelemfun  13061  ennnfonelemf1  13062  ennnfonelemim  13068  exmidunben  13070  ctiunctlemfo  13083  omiunct  13088  ssnnctlemct  13090  isstruct2r  13116  prdsval  13379  ismgm  13463  issgrp  13509  sgrppropd  13519  sgrpidmndm  13526  mndpropd  13546  issubmnd  13548  prdsidlem  13553  resmhm2b  13595  gsumwmhm  13604  isgrpinv  13660  grplmulf1o  13680  dfgrp3mlem  13704  grplactcnv  13708  pwssub  13719  mhmid  13725  mhmmnd  13726  ghmgrp  13728  mulgval  13732  mulgfng  13734  mulgnnp1  13740  mulgnn0dir  13762  mulgneg2  13766  mhmmulg  13773  grpissubg  13804  isnsg  13812  isnsg3  13817  nmzsubg  13820  ghmmhmb  13864  ghmpreima  13876  ghmnsgpreima  13879  ghmf1  13883  ghmf1o  13885  conjghm  13886  conjnmz  13889  conjnmzb  13890  ghmcmn  13937  gsumfzconst  13951  issrg  14002  srglmhm  14030  srgrmhm  14031  isring  14037  ringadd2  14064  ringlghm  14098  ringrghm  14099  oppr1g  14119  dvdsrvald  14131  dvdsrd  14132  dvdsrex  14136  dvdsrmul1  14140  unitgrp  14154  rhmopp  14214  subrgintm  14281  subrgpropd  14291  isdomn  14307  lmodprop2d  14386  lssvacl  14403  lssvsubcl  14404  lssvscl  14413  lsslss  14419  lss1d  14421  lsspropdg  14469  expghmap  14645  mulgghm2  14646  znunit  14697  znrrg  14698  mplvalcoe  14733  mplsubgfilemcl  14742  mplsubgfileminv  14743  mplsubgfi  14744  opnssneib  14909  restbasg  14921  restopn2  14936  iscnp4  14971  cnss2  14980  cnconst2  14986  cnptopresti  14991  cnptoprest2  14993  neitx  15021  uptx  15027  txrest  15029  txdis1cn  15031  xmetres2  15132  xblss2ps  15157  blhalf  15161  blssps  15180  blss  15181  blssexps  15182  blssex  15183  blin2  15185  metequiv2  15249  bdmetval  15253  metcnp3  15264  metcnp  15265  metcn  15267  metcnpi  15268  metcnpi2  15269  txmetcnp  15271  txmetcn  15272  qtopbas  15275  tgqioo  15308  mpomulcn  15319  fsumcncntop  15320  elcncf2  15327  mulcncflem  15360  mulcncf  15361  suplociccreex  15377  limcdifap  15415  cnplimcim  15420  cnplimccntop  15423  limccnpcntop  15428  dvcj  15462  dvmptfsum  15478  dveflem  15479  ply1termlem  15495  plyaddlem1  15500  plymullem1  15501  plycolemc  15511  plycjlemc  15513  plyrecj  15516  dvply1  15518  reeff1olem  15524  eflt  15528  sin0pilem1  15534  ptolemy  15577  coseq0q4123  15587  coseq0negpitopi  15589  cos02pilt1  15604  cos11  15606  ioocosf1o  15607  rpcxpmul2  15666  cxplt  15669  cxple  15670  cxplt3  15673  apcxp2  15692  rprelogbmul  15708  rprelogbdiv  15710  dvdsppwf1o  15742  perfect  15754  lgsval  15762  lgsfcl2  15764  lgscllem  15765  lgsval2lem  15768  lgsdir2lem4  15789  lgsdir2lem5  15790  lgsdir2  15791  lgsne0  15796  gausslemma2dlem1a  15816  gausslemma2dlem1f1o  15818  2sqlem6  15878  2sqlem10  15883  umgrnloopv  15994  umgrvad2edg  16091  usgr1eop  16125  wlkvtxiedg  16225  wlkvtxiedgg  16226  upgredginwlk  16236  upgriswlkdc  16240  clwwlkccatlem  16280  eupth2lem3lem4fi  16353  pw1ndom3  16649  2omap  16654  pw1map  16656  pwle2  16659  pwf1oexmid  16660  subctctexmid  16661  pw1nct  16664  peano4nninf  16671  nninfalllem1  16673  nninfall  16674  nninfsellemeq  16679  nninfsellemqall  16680  nnnninfex  16687  nninfnfiinf  16688  sbthom  16693  refeq  16695  isomninnlem  16701  trilpolemeq1  16711  trilpolemlt1  16712  trirec0  16715  apdiff  16719  iswomninnlem  16721  ismkvnnlem  16724  redcwlpolemeq1  16726  ltlenmkv  16742  gfsumcl  16755