Theorem simplr 533

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 493	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  1092  simp2lr  1096  simp3lr  1100  bilukdc  1445  dcun  3637  ifnefals  3685  ifeqeqxdc  3687  intab  3997  exmid01  4333  exmidundif  4341  exmidundifim  4342  frirrg  4493  reg2exmidlema  4679  imadiflem  5458  fvco4  5774  fvmptt  5794  fcoconst  5873  funopsn  5885  f1imass  5974  fcof1  5983  fliftfun  5996  riotass2  6061  ovmpodxf  6208  fsuppeq  6481  fsuppeqg  6482  suppssdc  6494  suppssfvg  6497  dftpos4  6528  tfrlem1  6573  tfrlem3ag  6574  tfrlemibacc  6591  tfrlemibfn  6593  tfrlemi1  6597  tfrlemi14d  6598  tfr1onlem3ag  6602  tfr1onlembacc  6607  tfr1onlembfn  6609  tfr1onlemaccex  6613  tfrcllembacc  6620  tfrcllembfn  6622  tfrcllemaccex  6626  frecabcl  6664  nntr2  6770  dcdifsnid  6771  nnm00  6797  ecopovsymg  6902  ecopoverg  6904  th3qlem1  6905  mapss  6967  f1imaen2g  7074  pw2f1odclem  7128  xpen  7139  xpmapenlem  7143  mapunen  7145  phpm  7161  fidifsnen  7166  dif1enen  7178  fiunsnnn  7179  fin0  7183  fin0or  7184  findcard2d  7189  findcard2sd  7190  diffifi  7192  isinfinf  7195  tridc  7198  fimax2gtrilemstep  7199  fimax2gtri  7200  en2eqpr  7208  onunsnss  7218  unsnfidcex  7221  unsnfidcel  7222  undifdcss  7224  unfiin  7227  fisseneq  7236  ssfirab  7238  f1finf1o  7258  fidcenumlemrks  7264  fidcenumlemrk  7265  fidcenumlemr  7266  fidcenum  7267  ffsuppbi  7294  fdcf1  7310  f1setfi  7311  2omap  7312  suplub2ti  7335  supisolem  7342  ordiso2  7369  djudom  7427  omp1eomlem  7428  difinfsnlem  7433  difinfinf  7435  ctm  7443  ctssdclemn0  7444  enumct  7449  nnnninfeq  7462  nnnninfeq2  7463  nninfisol  7467  enomnilem  7472  finomni  7474  exmidomni  7476  fodju0  7481  ismkvnex  7489  enmkvlem  7495  enwomnilem  7503  pr2cv1  7535  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidaclem  7558  exmidontriimlem1  7571  exmidontriimlem2  7572  exmidontriimlem3  7573  exmidontriimlem4  7574  exmidontriim  7575  netap  7614  exmidapne  7620  dfplpq2  7715  dfmpq2  7716  mulpipqqs  7734  nqpi  7739  distrnqg  7748  prarloclemarch  7779  enq0tr  7795  nqnq0pi  7799  nq0nn  7803  nnnq0lem1  7807  prarloclemup  7856  prarloclem3  7858  prarloclemcalc  7863  genplt2i  7871  addnqprllem  7888  addnqprulem  7889  appdivnq  7924  distrlem1prl  7943  distrlem1pru  7944  ltaddpr  7958  ltexprlemlol  7963  ltexprlemupu  7965  ltexprlemdisj  7967  addcanprleml  7975  ltaprlem  7979  addextpr  7982  recexprlemopu  7988  recexprlemdisj  7991  recexprlem1ssl  7994  aptiprleml  8000  cauappcvgprlemm  8006  cauappcvgprlemopl  8007  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemdisj  8012  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemm  8029  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemladdfu  8038  caucvgprprlemml  8055  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemexbt  8067  suplocexprlemru  8080  suplocexprlemloc  8082  suplocexprlemub  8084  suplocexprlemlub  8085  prsrlem1  8103  recexgt0sr  8134  mulgt0sr  8139  archsr  8143  caucvgsrlemcau  8154  caucvgsrlemoffcau  8159  caucvgsrlemoffres  8161  suplocsrlemb  8167  suplocsrlempr  8168  suplocsrlem  8169  addcnsr  8195  mulcnsr  8196  mulcnsrec  8204  axmulcom  8232  nntopi  8255  axcaucvglemcau  8259  axcaucvglemres  8260  axpre-suploclemres  8262  axpre-suploc  8263  mpomulf  8310  axsuploc  8392  ltntri  8448  cnegexlem2  8496  cnegexlem3  8497  addsub4  8563  le2add  8766  lt2add  8767  lt2sub  8782  le2sub  8783  rereim  8908  apreim  8925  mulreim  8926  apcotr  8929  apadd1  8930  addext  8932  mulext1  8934  mulext  8936  apti  8944  aptap  8972  receuap  8993  rec11rap  9035  divdivdivap  9037  divadddivap  9051  divsubdivap  9052  rerecclap  9054  recgt0  9174  prodgt0gt0  9175  prodgt0  9176  prodge0  9178  lemulge11  9190  lt2mul2div  9203  ltrec  9207  lerec  9208  ltrec1  9212  lediv2a  9219  mulle0r  9268  sup3exmid  9281  zdiv  9717  eluzuzle  9913  supinfneg  9978  infsupneg  9979  infregelbex  9981  xrltso  10181  xnn0dcle  10187  xnn0letri  10188  npnflt  10200  nmnfgt  10203  z2ge  10211  xaddf  10229  xaddval  10230  xpncan  10256  xleadd1a  10258  xltadd1  10261  xaddge0  10263  xle2add  10264  xleaddadd  10272  ixxss1  10289  ixxss2  10290  elico2  10322  iccsupr  10351  fzass4  10451  fzrev  10474  fz0fzelfz0  10517  fzocatel  10600  elfzomelpfzo  10632  zsupcllemstep  10645  exbtwnzlemstep  10665  rebtwn2zlemstep  10670  qbtwnxr  10675  xqltnle  10685  apbtwnz  10692  btwnzge0  10718  modqid  10769  modqcyc  10779  modqcyc2  10780  modqaddabs  10782  modqaddmod  10783  mulqaddmodid  10784  modqmuladd  10786  modqltm1p1mod  10796  modqsubmod  10802  modqsubmodmod  10803  modaddmodlo  10808  modqmulmod  10809  modqmulmodr  10810  modqsubdir  10813  addmodlteq  10818  nninfinf  10863  iseqf1olemab  10922  iseqf1olemmo  10925  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  seqf1oglem1  10939  seqf1oglem2  10940  seqf1og  10941  exp3val  10961  expcl2lemap  10971  expap0  10989  expnegzap  10993  expmul  11004  leexp1a  11014  qsqeqor  11070  resq01  11078  expnbnd  11084  nn0ltexp2  11130  nn0opth2  11145  facndiv  11160  faclbnd  11162  bcval5  11184  bcpasc  11187  hashennnuni  11201  hashunlem  11227  hashunsng  11231  hashprg  11232  fiprsshashgt1  11241  hashxp  11250  fimaxq  11253  hashfibc  11266  zfz1isolemiso  11274  zfz1isolem1  11275  seq3coll  11277  iswrdiz  11294  wrdnval  11318  ccatlen  11346  ccatvalfn  11352  ccatsymb  11353  ccatalpha  11364  ccat2s1fstg  11399  swrdclg  11405  swrdsb0eq  11420  pfxwrdsymbg  11445  wrdind  11477  wrd2ind  11478  swrdccatin2  11484  pfxccatin12lem2  11486  pfxccatin12  11488  pfxccat3  11489  swrdccat  11490  shftlem  11564  shftfvalg  11566  shftfval  11569  2shfti  11579  caucvgrelemrec  11728  caucvgrelemcau  11729  caucvgre  11730  cvg1nlemcau  11733  cvg1nlemres  11734  resqrexlemcalc3  11765  resqrexlemcvg  11768  resqrexlemglsq  11771  resqrexlemga  11772  sqrtsq  11793  leabs  11823  absexpzap  11829  abslt  11837  absle  11838  abssubap0  11839  caubnd2  11866  icodiamlt  11929  maxleim  11954  maxabslemval  11957  maxleastlt  11964  rexico  11970  zmaxcl  11973  fimaxre2  11976  minmax  11979  xrmaxleim  11993  xrmaxiflemcl  11994  xrmaxifle  11995  xrmaxiflemlub  11997  xrmaxiflemval  11999  xrmaxleastlt  12005  xrmaxltsup  12007  xrmaxadd  12010  xrminmax  12014  xrbdtri  12025  climuni  12042  climshftlemg  12051  iserex  12088  climcau  12096  climrecvg1n  12097  climcvg1nlem  12098  sumeq2  12108  summodclem3  12130  zsumdc  12134  isumss  12141  fisumss  12142  sumsnf  12159  fsumconst  12204  modfsummod  12208  fsum00  12212  fsumabs  12215  fsumrelem  12221  fsumiun  12227  isumsplit  12241  divcnv  12247  geo2sum  12264  geoisumr  12268  cvgratz  12282  ntrivcvgap  12298  prodeq2  12307  prodmodclem2  12327  prodmodc  12328  zproddc  12329  fprodmul  12341  prodsnf  12342  fprodcl2lem  12355  fprodconst  12370  fprodap0  12371  fprodrec  12379  fprodap0f  12386  fprodle  12390  fprodmodd  12391  tanaddap  12489  zdvdsdc  12562  dvds2ln  12574  fsumdvds  12592  dvdsle  12594  dvdsext  12605  divalglemeunn  12671  divalglemex  12672  divalglemeuneg  12673  bitsfzo  12705  bitsmod  12706  bitsinv1lem  12711  bitsinv1  12712  dvdsbnd  12716  gcdsupex  12717  gcdsupcl  12718  dvdslegcd  12724  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlemzz  12762  bezoutlembz  12764  bezoutlembi  12765  bezoutlemle  12768  dfgcd3  12770  bezout  12771  dfgcd2  12774  dvdsmulgcd  12785  bezoutr  12792  uzwodc  12797  nninfctlemfo  12800  lcmval  12824  lcmcllem  12828  lcmneg  12835  ncoprmgcdne1b  12850  isprm2lem  12877  prmind2  12881  dvdsnprmd  12886  isprm5  12903  prmdvdsexp  12909  sqrt2irr  12923  oddpwdclemxy  12930  oddpwdclemdc  12934  nonsq  12968  pceu  13057  pcmul  13063  pc2dvds  13092  pcz  13094  pcprmpw2  13095  dvdsprmpweqle  13099  pcfac  13112  qexpz  13114  prmpwdvds  13117  1arith  13129  mul4sq  13156  4sqexercise2  13161  4sqlemsdc  13162  ballotfilem2  13211  ballotfilemsle  13231  ballotfilemsdom  13238  ballotfilemsima  13242  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemhom  13289  ennnfonelemfun  13291  ennnfonelemf1  13292  ennnfonelemim  13298  exmidunben  13300  ctiunctlemfo  13313  omiunct  13318  ssnnctlemct  13320  isstruct2r  13346  ismgm  13660  issgrp  13701  sgrppropd  13711  sgrpidmndm  13716  mndpropd  13736  issubmnd  13738  resmhm2b  13779  gzsumwmhm  13786  isgrpinv  13842  grplmulf1o  13862  dfgrp3mlem  13886  grplactcnv  13890  mhmid  13901  mhmmnd  13902  ghmgrp  13904  mulgval  13908  mulgfng  13910  mulgnnp1  13916  mulgnn0dir  13938  mulgneg2  13942  mhmmulg  13949  grpissubg  13980  isnsg  13988  isnsg3  13993  nmzsubg  13996  ghmmhmb  14040  ghmpreima  14052  ghmnsgpreima  14055  ghmf1  14059  ghmf1o  14061  conjghm  14062  conjnmz  14065  conjnmzb  14066  ghmcmn  14114  gzsumconst  14126  gsumzfi  14141  gsumclfi  14142  gsummptfidmadd  14144  gsumsubmclfi  14146  gsumconstcmn  14149  prdsval  14156  prdsidlem  14176  pwssub  14199  issrg  14252  srglmhm  14280  srgrmhm  14281  isring  14287  ringadd2  14315  ringlghm  14349  ringrghm  14350  oppr1g  14371  dvdsrvald  14383  dvdsrd  14384  dvdsrex  14388  dvdsrmul1  14392  unitgrp  14406  rhmopp  14466  subrgintm  14534  subrgpropd  14544  isdomn  14561  aprnzr  14582  opprdrng  14603  lmodprop2d  14668  lssvacl  14685  lssvsubcl  14686  lssvscl  14695  lsslss  14701  lss1d  14703  lsspropdg  14751  gsumfsum  14906  expghmap  14925  mulgghm2  14926  znunit  14977  znrrg  14978  issubassa2  15018  assamulgscmlem1  15024  assamulgscmlem2  15025  mplvalcoe  15064  mplsubgfilemcl  15073  mplsubgfileminv  15074  mplsubgfi  15075  opnssneib  15240  restbasg  15252  restopn2  15267  iscnp4  15302  cnss2  15311  cnconst2  15317  cnptopresti  15322  cnptoprest2  15324  neitx  15352  uptx  15358  txrest  15360  txdis1cn  15362  xmetres2  15463  xblss2ps  15488  blhalf  15492  blssps  15511  blss  15512  blssexps  15513  blssex  15514  blin2  15516  metequiv2  15580  bdmetval  15584  metcnp3  15595  metcnp  15596  metcn  15598  metcnpi  15599  metcnpi2  15600  txmetcnp  15602  txmetcn  15603  qtopbas  15606  tgqioo  15639  mpomulcn  15650  fsumcncntop  15651  elcncf2  15658  mulcncflem  15691  mulcncf  15692  suplociccreex  15708  limcdifap  15746  cnplimcim  15751  cnplimccntop  15754  limccnpcntop  15759  dvcj  15793  dvmptfsum  15809  dveflem  15810  ply1termlem  15826  plyaddlem1  15831  plymullem1  15832  plycolemc  15842  plycjlemc  15844  plyrecj  15847  dvply1  15849  reeff1olem  15855  eflt  15859  sin0pilem1  15865  ptolemy  15908  coseq0q4123  15918  coseq0negpitopi  15920  cos02pilt1  15935  cos11  15937  ioocosf1o  15938  rpcxpmul2  15998  cxplt  16001  cxple  16002  cxplt3  16005  apcxp2  16024  rprelogbmul  16040  rprelogbdiv  16042  birthdaylem3  16072  pellexlem3  16076  dvdsppwf1o  16086  perfect  16098  lgsval  16106  lgsfcl2  16108  lgscllem  16109  lgsval2lem  16112  lgsdir2lem4  16133  lgsdir2lem5  16134  lgsdir2  16135  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  2sqlem6  16222  2sqlem10  16227  umgrnloopv  16338  umgrvad2edg  16435  usgr1eop  16469  wlkvtxiedg  16569  wlkvtxiedgg  16570  upgredginwlk  16580  upgriswlkdc  16584  clwwlkccatlem  16624  eupth2lem3lem4fi  16697  pw1ndom3  17003  pw1map  17008  pwle2  17011  pwf1oexmid  17012  subctctexmid  17013  pw1nct  17016  peano4nninf  17023  nninfalllem1  17025  nninfall  17026  nninfsellemeq  17031  nninfsellemqall  17032  nnnninfex  17039  nninfnfiinf  17040  sbthom  17045  refeq  17047  isomninnlem  17053  trilpolemeq1  17063  trilpolemlt1  17064  trirec0  17067  apdiff  17071  iswomninnlem  17073  ismkvnnlem  17076  redcwlpolemeq1  17078  ltlenmkv  17094