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  1088  simp2lr  1092  simp3lr  1096  bilukdc  1441  dcun  3618  ifnefals  3666  intab  3977  exmid01  4310  exmidundif  4318  exmidundifim  4319  frirrg  4470  reg2exmidlema  4655  imadiflem  5434  fvco4  5748  fvmptt  5768  fcoconst  5847  funopsn  5859  f1imass  5946  fcof1  5955  fliftfun  5968  riotass2  6031  ovmpodxf  6178  fsuppeq  6446  fsuppeqg  6447  suppssdc  6459  suppssfvg  6462  dftpos4  6493  tfrlem1  6538  tfrlem3ag  6539  tfrlemibacc  6556  tfrlemibfn  6558  tfrlemi1  6562  tfrlemi14d  6563  tfr1onlem3ag  6567  tfr1onlembacc  6572  tfr1onlembfn  6574  tfr1onlemaccex  6578  tfrcllembacc  6585  tfrcllembfn  6587  tfrcllemaccex  6591  frecabcl  6629  nntr2  6735  dcdifsnid  6736  nnm00  6762  ecopovsymg  6867  ecopoverg  6869  th3qlem1  6870  mapss  6925  f1imaen2g  7032  pw2f1odclem  7086  xpen  7097  xpmapenlem  7101  mapunen  7103  phpm  7119  fidifsnen  7124  dif1enen  7136  fiunsnnn  7137  fin0  7141  fin0or  7142  findcard2d  7147  findcard2sd  7148  diffifi  7150  isinfinf  7153  tridc  7156  fimax2gtrilemstep  7157  fimax2gtri  7158  en2eqpr  7166  onunsnss  7176  unsnfidcex  7179  unsnfidcel  7180  undifdcss  7182  unfiin  7185  fisseneq  7194  ssfirab  7196  f1finf1o  7216  fidcenumlemrks  7222  fidcenumlemrk  7223  fidcenumlemr  7224  fidcenum  7225  ffsuppbi  7252  2omap  7268  suplub2ti  7291  supisolem  7298  ordiso2  7325  djudom  7383  omp1eomlem  7384  difinfsnlem  7389  difinfinf  7391  ctm  7399  ctssdclemn0  7400  enumct  7405  nnnninfeq  7418  nnnninfeq2  7419  nninfisol  7423  enomnilem  7428  finomni  7430  exmidomni  7432  fodju0  7437  ismkvnex  7445  enmkvlem  7451  enwomnilem  7459  pr2cv1  7491  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidaclem  7514  exmidontriimlem1  7527  exmidontriimlem2  7528  exmidontriimlem3  7529  exmidontriimlem4  7530  exmidontriim  7531  netap  7564  exmidapne  7570  dfplpq2  7665  dfmpq2  7666  mulpipqqs  7684  nqpi  7689  distrnqg  7698  prarloclemarch  7729  enq0tr  7745  nqnq0pi  7749  nq0nn  7753  nnnq0lem1  7757  prarloclemup  7806  prarloclem3  7808  prarloclemcalc  7813  genplt2i  7821  addnqprllem  7838  addnqprulem  7839  appdivnq  7874  distrlem1prl  7893  distrlem1pru  7894  ltaddpr  7908  ltexprlemlol  7913  ltexprlemupu  7915  ltexprlemdisj  7917  addcanprleml  7925  ltaprlem  7929  addextpr  7932  recexprlemopu  7938  recexprlemdisj  7941  recexprlem1ssl  7944  aptiprleml  7950  cauappcvgprlemm  7956  cauappcvgprlemopl  7957  cauappcvgprlemlol  7958  cauappcvgprlemopu  7959  cauappcvgprlemdisj  7962  cauappcvgprlemladdfu  7965  cauappcvgprlemladdfl  7966  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  caucvgprlemm  7979  caucvgprlemopl  7980  caucvgprlemlol  7981  caucvgprlemopu  7982  caucvgprlemladdfu  7988  caucvgprprlemml  8005  caucvgprprlemopl  8008  caucvgprprlemlol  8009  caucvgprprlemopu  8010  caucvgprprlemexbt  8017  suplocexprlemru  8030  suplocexprlemloc  8032  suplocexprlemub  8034  suplocexprlemlub  8035  prsrlem1  8053  recexgt0sr  8084  mulgt0sr  8089  archsr  8093  caucvgsrlemcau  8104  caucvgsrlemoffcau  8109  caucvgsrlemoffres  8111  suplocsrlemb  8117  suplocsrlempr  8118  suplocsrlem  8119  addcnsr  8145  mulcnsr  8146  mulcnsrec  8154  axmulcom  8182  nntopi  8205  axcaucvglemcau  8209  axcaucvglemres  8210  axpre-suploclemres  8212  axpre-suploc  8213  mpomulf  8260  axsuploc  8342  ltntri  8397  cnegexlem2  8445  cnegexlem3  8446  addsub4  8512  le2add  8714  lt2add  8715  lt2sub  8730  le2sub  8731  rereim  8856  apreim  8873  mulreim  8874  apcotr  8877  apadd1  8878  addext  8880  mulext1  8882  mulext  8884  apti  8892  aptap  8920  receuap  8939  rec11rap  8981  divdivdivap  8983  divadddivap  8997  divsubdivap  8998  rerecclap  9000  recgt0  9120  prodgt0gt0  9121  prodgt0  9122  prodge0  9124  lemulge11  9136  lt2mul2div  9149  ltrec  9153  lerec  9154  ltrec1  9158  lediv2a  9165  mulle0r  9214  sup3exmid  9227  zdiv  9662  eluzuzle  9858  supinfneg  9923  infsupneg  9924  infregelbex  9926  xrltso  10125  xnn0dcle  10131  xnn0letri  10132  npnflt  10144  nmnfgt  10147  z2ge  10155  xaddf  10173  xaddval  10174  xpncan  10200  xleadd1a  10202  xltadd1  10205  xaddge0  10207  xle2add  10208  xleaddadd  10216  ixxss1  10233  ixxss2  10234  elico2  10266  iccsupr  10295  fzass4  10392  fzrev  10414  fz0fzelfz0  10457  fzocatel  10540  elfzomelpfzo  10572  zsupcllemstep  10585  exbtwnzlemstep  10603  rebtwn2zlemstep  10608  qbtwnxr  10613  xqltnle  10623  apbtwnz  10630  btwnzge0  10656  modqid  10707  modqcyc  10717  modqcyc2  10718  modqaddabs  10720  modqaddmod  10721  mulqaddmodid  10722  modqmuladd  10724  modqltm1p1mod  10734  modqsubmod  10740  modqsubmodmod  10741  modaddmodlo  10746  modqmulmod  10747  modqmulmodr  10748  modqsubdir  10751  addmodlteq  10756  nninfinf  10801  iseqf1olemab  10860  iseqf1olemmo  10863  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  seqf1oglem1  10877  seqf1oglem2  10878  seqf1og  10879  exp3val  10899  expcl2lemap  10909  expap0  10927  expnegzap  10931  expmul  10942  leexp1a  10952  qsqeqor  11008  expnbnd  11021  nn0ltexp2  11067  nn0opth2  11082  facndiv  11097  faclbnd  11099  bcval5  11121  bcpasc  11124  hashennnuni  11137  hashunlem  11163  hashunsng  11167  hashprg  11168  fiprsshashgt1  11177  hashxp  11186  fimaxq  11187  hashfibc  11200  zfz1isolemiso  11204  zfz1isolem1  11205  seq3coll  11207  iswrdiz  11224  wrdnval  11248  ccatlen  11276  ccatvalfn  11282  ccatsymb  11283  ccatalpha  11294  ccat2s1fstg  11329  swrdclg  11335  swrdsb0eq  11350  pfxwrdsymbg  11375  wrdind  11407  wrd2ind  11408  swrdccatin2  11414  pfxccatin12lem2  11416  pfxccatin12  11418  pfxccat3  11419  swrdccat  11420  shftlem  11494  shftfvalg  11496  shftfval  11499  2shfti  11509  caucvgrelemrec  11657  caucvgrelemcau  11658  caucvgre  11659  cvg1nlemcau  11662  cvg1nlemres  11663  resqrexlemcalc3  11694  resqrexlemcvg  11697  resqrexlemglsq  11700  resqrexlemga  11701  sqrtsq  11722  leabs  11752  absexpzap  11758  abslt  11766  absle  11767  abssubap0  11768  caubnd2  11795  icodiamlt  11858  maxleim  11883  maxabslemval  11886  maxleastlt  11893  rexico  11899  zmaxcl  11902  fimaxre2  11905  minmax  11908  xrmaxleim  11922  xrmaxiflemcl  11923  xrmaxifle  11924  xrmaxiflemlub  11926  xrmaxiflemval  11928  xrmaxleastlt  11934  xrmaxltsup  11936  xrmaxadd  11939  xrminmax  11943  xrbdtri  11954  climuni  11971  climshftlemg  11980  iserex  12017  climcau  12025  climrecvg1n  12026  climcvg1nlem  12027  sumeq2  12037  summodclem3  12059  zsumdc  12063  isumss  12070  fisumss  12071  sumsnf  12088  fsumconst  12133  modfsummod  12137  fsum00  12141  fsumabs  12144  fsumrelem  12150  fsumiun  12156  isumsplit  12170  divcnv  12176  geo2sum  12193  geoisumr  12197  cvgratz  12211  ntrivcvgap  12227  prodeq2  12236  prodmodclem2  12256  prodmodc  12257  zproddc  12258  fprodmul  12270  prodsnf  12271  fprodcl2lem  12284  fprodconst  12299  fprodap0  12300  fprodrec  12308  fprodap0f  12315  fprodle  12319  fprodmodd  12320  tanaddap  12418  zdvdsdc  12491  dvds2ln  12503  fsumdvds  12521  dvdsle  12523  dvdsext  12534  divalglemeunn  12600  divalglemex  12601  divalglemeuneg  12602  bitsfzo  12634  bitsmod  12635  bitsinv1lem  12640  bitsinv1  12641  dvdsbnd  12645  gcdsupex  12646  gcdsupcl  12647  dvdslegcd  12653  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemmain  12687  bezoutlemzz  12691  bezoutlembz  12693  bezoutlembi  12694  bezoutlemle  12697  dfgcd3  12699  bezout  12700  dfgcd2  12703  dvdsmulgcd  12714  bezoutr  12721  uzwodc  12726  nninfctlemfo  12729  lcmval  12753  lcmcllem  12757  lcmneg  12764  ncoprmgcdne1b  12779  isprm2lem  12806  prmind2  12810  dvdsnprmd  12815  isprm5  12832  prmdvdsexp  12838  sqrt2irr  12852  oddpwdclemxy  12859  oddpwdclemdc  12863  nonsq  12897  pceu  12986  pcmul  12992  pc2dvds  13021  pcz  13023  pcprmpw2  13024  dvdsprmpweqle  13028  pcfac  13041  qexpz  13043  prmpwdvds  13046  1arith  13058  mul4sq  13085  4sqexercise2  13090  4sqlemsdc  13091  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemhom  13155  ennnfonelemfun  13157  ennnfonelemf1  13158  ennnfonelemim  13164  exmidunben  13166  ctiunctlemfo  13179  omiunct  13184  ssnnctlemct  13186  isstruct2r  13212  prdsval  13475  ismgm  13559  issgrp  13605  sgrppropd  13615  sgrpidmndm  13622  mndpropd  13642  issubmnd  13644  prdsidlem  13649  resmhm2b  13691  gsumwmhm  13700  isgrpinv  13756  grplmulf1o  13776  dfgrp3mlem  13800  grplactcnv  13804  pwssub  13815  mhmid  13821  mhmmnd  13822  ghmgrp  13824  mulgval  13828  mulgfng  13830  mulgnnp1  13836  mulgnn0dir  13858  mulgneg2  13862  mhmmulg  13869  grpissubg  13900  isnsg  13908  isnsg3  13913  nmzsubg  13916  ghmmhmb  13960  ghmpreima  13972  ghmnsgpreima  13975  ghmf1  13979  ghmf1o  13981  conjghm  13982  conjnmz  13985  conjnmzb  13986  ghmcmn  14033  gsumfzconst  14047  issrg  14098  srglmhm  14126  srgrmhm  14127  isring  14133  ringadd2  14160  ringlghm  14194  ringrghm  14195  oppr1g  14215  dvdsrvald  14227  dvdsrd  14228  dvdsrex  14232  dvdsrmul1  14236  unitgrp  14250  rhmopp  14310  subrgintm  14377  subrgpropd  14387  isdomn  14404  lmodprop2d  14483  lssvacl  14500  lssvsubcl  14501  lssvscl  14510  lsslss  14516  lss1d  14518  lsspropdg  14566  expghmap  14742  mulgghm2  14743  znunit  14794  znrrg  14795  mplvalcoe  14832  mplsubgfilemcl  14841  mplsubgfileminv  14842  mplsubgfi  14843  opnssneib  15008  restbasg  15020  restopn2  15035  iscnp4  15070  cnss2  15079  cnconst2  15085  cnptopresti  15090  cnptoprest2  15092  neitx  15120  uptx  15126  txrest  15128  txdis1cn  15130  xmetres2  15231  xblss2ps  15256  blhalf  15260  blssps  15279  blss  15280  blssexps  15281  blssex  15282  blin2  15284  metequiv2  15348  bdmetval  15352  metcnp3  15363  metcnp  15364  metcn  15366  metcnpi  15367  metcnpi2  15368  txmetcnp  15370  txmetcn  15371  qtopbas  15374  tgqioo  15407  mpomulcn  15418  fsumcncntop  15419  elcncf2  15426  mulcncflem  15459  mulcncf  15460  suplociccreex  15476  limcdifap  15514  cnplimcim  15519  cnplimccntop  15522  limccnpcntop  15527  dvcj  15561  dvmptfsum  15577  dveflem  15578  ply1termlem  15594  plyaddlem1  15599  plymullem1  15600  plycolemc  15610  plycjlemc  15612  plyrecj  15615  dvply1  15617  reeff1olem  15623  eflt  15627  sin0pilem1  15633  ptolemy  15676  coseq0q4123  15686  coseq0negpitopi  15688  cos02pilt1  15703  cos11  15705  ioocosf1o  15706  rpcxpmul2  15765  cxplt  15768  cxple  15769  cxplt3  15772  apcxp2  15791  rprelogbmul  15807  rprelogbdiv  15809  pellexlem3  15834  dvdsppwf1o  15844  perfect  15856  lgsval  15864  lgsfcl2  15866  lgscllem  15867  lgsval2lem  15870  lgsdir2lem4  15891  lgsdir2lem5  15892  lgsdir2  15893  lgsne0  15898  gausslemma2dlem1a  15918  gausslemma2dlem1f1o  15920  2sqlem6  15980  2sqlem10  15985  umgrnloopv  16096  umgrvad2edg  16193  usgr1eop  16227  wlkvtxiedg  16327  wlkvtxiedgg  16328  upgredginwlk  16338  upgriswlkdc  16342  clwwlkccatlem  16382  eupth2lem3lem4fi  16455  pw1ndom3  16751  pw1map  16756  pwle2  16759  pwf1oexmid  16760  subctctexmid  16761  pw1nct  16764  peano4nninf  16771  nninfalllem1  16773  nninfall  16774  nninfsellemeq  16779  nninfsellemqall  16780  nnnninfex  16787  nninfnfiinf  16788  sbthom  16793  refeq  16795  isomninnlem  16801  trilpolemeq1  16811  trilpolemlt1  16812  trirec0  16815  apdiff  16819  iswomninnlem  16821  ismkvnnlem  16824  redcwlpolemeq1  16826  ltlenmkv  16842  gfsumz  16855  gfsumcl  16856