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  1063  simp2lr  1067  simp3lr  1071  bilukdc  1407  dcun  3556  ifnefals  3599  intab  3899  exmid01  4227  exmidundif  4235  exmidundifim  4236  frirrg  4381  reg2exmidlema  4566  imadiflem  5333  fvco4  5629  fvmptt  5649  fcoconst  5729  f1imass  5817  fcof1  5826  fliftfun  5839  riotass2  5900  ovmpodxf  6044  dftpos4  6316  tfrlem1  6361  tfrlem3ag  6362  tfrlemibacc  6379  tfrlemibfn  6381  tfrlemi1  6385  tfrlemi14d  6386  tfr1onlem3ag  6390  tfr1onlembacc  6395  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfrcllembacc  6408  tfrcllembfn  6410  tfrcllemaccex  6414  frecabcl  6452  nntr2  6556  dcdifsnid  6557  nnm00  6583  ecopovsymg  6688  ecopoverg  6690  th3qlem1  6691  mapss  6745  f1imaen2g  6847  pw2f1odclem  6890  xpen  6901  xpmapenlem  6905  phpm  6921  fidifsnen  6926  dif1enen  6936  fiunsnnn  6937  fin0  6941  fin0or  6942  findcard2d  6947  findcard2sd  6948  diffifi  6950  isinfinf  6953  tridc  6955  fimax2gtrilemstep  6956  fimax2gtri  6957  en2eqpr  6963  onunsnss  6973  unsnfidcex  6976  unsnfidcel  6977  undifdcss  6979  unfiin  6982  fisseneq  6988  ssfirab  6990  f1finf1o  7006  fidcenumlemrks  7012  fidcenumlemrk  7013  fidcenumlemr  7014  fidcenum  7015  suplub2ti  7060  supisolem  7067  ordiso2  7094  djudom  7152  omp1eomlem  7153  difinfsnlem  7158  difinfinf  7160  ctm  7168  ctssdclemn0  7169  enumct  7174  nnnninfeq  7187  nnnninfeq2  7188  nninfisol  7192  enomnilem  7197  finomni  7199  exmidomni  7201  fodju0  7206  ismkvnex  7214  enmkvlem  7220  enwomnilem  7228  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  exmidontriimlem1  7281  exmidontriimlem2  7282  exmidontriimlem3  7283  exmidontriimlem4  7284  exmidontriim  7285  netap  7314  exmidapne  7320  dfplpq2  7414  dfmpq2  7415  mulpipqqs  7433  nqpi  7438  distrnqg  7447  prarloclemarch  7478  enq0tr  7494  nqnq0pi  7498  nq0nn  7502  nnnq0lem1  7506  prarloclemup  7555  prarloclem3  7557  prarloclemcalc  7562  genplt2i  7570  addnqprllem  7587  addnqprulem  7588  appdivnq  7623  distrlem1prl  7642  distrlem1pru  7643  ltaddpr  7657  ltexprlemlol  7662  ltexprlemupu  7664  ltexprlemdisj  7666  addcanprleml  7674  ltaprlem  7678  addextpr  7681  recexprlemopu  7687  recexprlemdisj  7690  recexprlem1ssl  7693  aptiprleml  7699  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemdisj  7711  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemladdfu  7737  caucvgprprlemml  7754  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemopu  7759  caucvgprprlemexbt  7766  suplocexprlemru  7779  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  prsrlem1  7802  recexgt0sr  7833  mulgt0sr  7838  archsr  7842  caucvgsrlemcau  7853  caucvgsrlemoffcau  7858  caucvgsrlemoffres  7860  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  addcnsr  7894  mulcnsr  7895  mulcnsrec  7903  axmulcom  7931  nntopi  7954  axcaucvglemcau  7958  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  mpomulf  8009  axsuploc  8092  ltntri  8147  cnegexlem2  8195  cnegexlem3  8196  addsub4  8262  le2add  8463  lt2add  8464  lt2sub  8479  le2sub  8480  rereim  8605  apreim  8622  mulreim  8623  apcotr  8626  apadd1  8627  addext  8629  mulext1  8631  mulext  8633  apti  8641  aptap  8669  receuap  8688  rec11rap  8730  divdivdivap  8732  divadddivap  8746  divsubdivap  8747  rerecclap  8749  recgt0  8869  prodgt0gt0  8870  prodgt0  8871  prodge0  8873  lemulge11  8885  lt2mul2div  8898  ltrec  8902  lerec  8903  ltrec1  8907  lediv2a  8914  mulle0r  8963  sup3exmid  8976  zdiv  9405  eluzuzle  9600  supinfneg  9660  infsupneg  9661  infregelbex  9663  xrltso  9862  xnn0dcle  9868  xnn0letri  9869  npnflt  9881  nmnfgt  9884  z2ge  9892  xaddf  9910  xaddval  9911  xpncan  9937  xleadd1a  9939  xltadd1  9942  xaddge0  9944  xle2add  9945  xleaddadd  9953  ixxss1  9970  ixxss2  9971  elico2  10003  iccsupr  10032  fzass4  10128  fzrev  10150  fz0fzelfz0  10193  fzocatel  10266  elfzomelpfzo  10298  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  qbtwnxr  10326  xqltnle  10336  apbtwnz  10343  btwnzge0  10369  modqid  10420  modqcyc  10430  modqcyc2  10431  modqaddabs  10433  modqaddmod  10434  mulqaddmodid  10435  modqmuladd  10437  modqltm1p1mod  10447  modqsubmod  10453  modqsubmodmod  10454  modaddmodlo  10459  modqmulmod  10460  modqmulmodr  10461  modqsubdir  10464  addmodlteq  10469  nninfinf  10514  iseqf1olemab  10573  iseqf1olemmo  10576  iseqf1olemjpcl  10579  iseqf1olemqpcl  10580  seqf1oglem1  10590  seqf1oglem2  10591  seqf1og  10592  exp3val  10612  expcl2lemap  10622  expap0  10640  expnegzap  10644  expmul  10655  leexp1a  10665  qsqeqor  10721  expnbnd  10734  nn0ltexp2  10780  nn0opth2  10795  facndiv  10810  faclbnd  10812  bcval5  10834  bcpasc  10837  hashennnuni  10850  hashunlem  10875  hashunsng  10878  hashprg  10879  fiprsshashgt1  10888  hashxp  10897  fimaxq  10898  zfz1isolemiso  10910  zfz1isolem1  10911  seq3coll  10913  iswrdiz  10921  wrdnval  10944  shftlem  10960  shftfvalg  10962  shftfval  10965  2shfti  10975  caucvgrelemrec  11123  caucvgrelemcau  11124  caucvgre  11125  cvg1nlemcau  11128  cvg1nlemres  11129  resqrexlemcalc3  11160  resqrexlemcvg  11163  resqrexlemglsq  11166  resqrexlemga  11167  sqrtsq  11188  leabs  11218  absexpzap  11224  abslt  11232  absle  11233  abssubap0  11234  caubnd2  11261  icodiamlt  11324  maxleim  11349  maxabslemval  11352  maxleastlt  11359  rexico  11365  zmaxcl  11368  fimaxre2  11370  minmax  11373  xrmaxleim  11387  xrmaxiflemcl  11388  xrmaxifle  11389  xrmaxiflemlub  11391  xrmaxiflemval  11393  xrmaxleastlt  11399  xrmaxltsup  11401  xrmaxadd  11404  xrminmax  11408  xrbdtri  11419  climuni  11436  climshftlemg  11445  iserex  11482  climcau  11490  climrecvg1n  11491  climcvg1nlem  11492  sumeq2  11502  summodclem3  11523  zsumdc  11527  isumss  11534  fisumss  11535  sumsnf  11552  fsumconst  11597  modfsummod  11601  fsum00  11605  fsumabs  11608  fsumrelem  11614  fsumiun  11620  isumsplit  11634  divcnv  11640  geo2sum  11657  geoisumr  11661  cvgratz  11675  ntrivcvgap  11691  prodeq2  11700  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodmul  11734  prodsnf  11735  fprodcl2lem  11748  fprodconst  11763  fprodap0  11764  fprodrec  11772  fprodap0f  11779  fprodle  11783  fprodmodd  11784  tanaddap  11882  zdvdsdc  11955  dvds2ln  11967  dvdsle  11986  dvdsext  11997  divalglemeunn  12062  divalglemex  12063  divalglemeuneg  12064  zsupcllemstep  12082  dvdsbnd  12093  gcdsupex  12094  gcdsupcl  12095  dvdslegcd  12101  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlemzz  12139  bezoutlembz  12141  bezoutlembi  12142  bezoutlemle  12145  dfgcd3  12147  bezout  12148  dfgcd2  12151  dvdsmulgcd  12162  bezoutr  12169  uzwodc  12174  nninfctlemfo  12177  lcmval  12201  lcmcllem  12205  lcmneg  12212  ncoprmgcdne1b  12227  isprm2lem  12254  prmind2  12258  dvdsnprmd  12263  isprm5  12280  prmdvdsexp  12286  sqrt2irr  12300  oddpwdclemxy  12307  oddpwdclemdc  12311  nonsq  12345  pceu  12433  pcmul  12439  pc2dvds  12468  pcz  12470  pcprmpw2  12471  dvdsprmpweqle  12475  pcfac  12488  qexpz  12490  prmpwdvds  12493  1arith  12505  mul4sq  12532  4sqexercise2  12537  4sqlemsdc  12538  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemhom  12572  ennnfonelemfun  12574  ennnfonelemf1  12575  ennnfonelemim  12581  exmidunben  12583  ctiunctlemfo  12596  omiunct  12601  ssnnctlemct  12603  isstruct2r  12629  ismgm  12940  issgrp  12986  sgrppropd  12996  sgrpidmndm  13001  mndpropd  13021  issubmnd  13023  resmhm2b  13061  gsumwmhm  13070  isgrpinv  13126  grplmulf1o  13146  dfgrp3mlem  13170  grplactcnv  13174  mhmid  13185  mhmmnd  13186  ghmgrp  13188  mulgval  13192  mulgfng  13194  mulgnnp1  13200  mulgnn0dir  13222  mulgneg2  13226  mhmmulg  13233  grpissubg  13264  isnsg  13272  isnsg3  13277  nmzsubg  13280  ghmmhmb  13324  ghmpreima  13336  ghmnsgpreima  13339  ghmf1  13343  ghmf1o  13345  conjghm  13346  conjnmz  13349  conjnmzb  13350  ghmcmn  13397  gsumfzconst  13411  issrg  13461  srglmhm  13489  srgrmhm  13490  isring  13496  ringadd2  13523  ringlghm  13557  ringrghm  13558  oppr1g  13578  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrd  13590  dvdsrex  13594  dvdsrmul1  13598  unitgrp  13612  rhmopp  13672  subrgintm  13739  subrgpropd  13749  isdomn  13765  lmodprop2d  13844  lssvacl  13861  lssvsubcl  13862  lssvscl  13871  lsslss  13877  lss1d  13879  lsspropdg  13927  expghmap  14095  mulgghm2  14096  znunit  14147  znrrg  14148  opnssneib  14324  restbasg  14336  restopn2  14351  iscnp4  14386  cnss2  14395  cnconst2  14401  cnptopresti  14406  cnptoprest2  14408  neitx  14436  uptx  14442  txrest  14444  txdis1cn  14446  xmetres2  14547  xblss2ps  14572  blhalf  14576  blssps  14595  blss  14596  blssexps  14597  blssex  14598  blin2  14600  metequiv2  14664  bdmetval  14668  metcnp3  14679  metcnp  14680  metcn  14682  metcnpi  14683  metcnpi2  14684  txmetcnp  14686  txmetcn  14687  qtopbas  14690  tgqioo  14715  fsumcncntop  14724  elcncf2  14729  mulcncflem  14761  mulcncf  14762  suplociccreex  14778  limcdifap  14816  cnplimcim  14821  cnplimccntop  14824  limccnpcntop  14829  dvcj  14858  dveflem  14872  ply1termlem  14888  plyaddlem1  14893  plymullem1  14894  reeff1olem  14906  eflt  14910  sin0pilem1  14916  ptolemy  14959  coseq0q4123  14969  coseq0negpitopi  14971  cos02pilt1  14986  cos11  14988  ioocosf1o  14989  cxplt  15050  cxple  15051  cxplt3  15054  apcxp2  15072  rprelogbmul  15087  rprelogbdiv  15089  lgsval  15120  lgsfcl2  15122  lgscllem  15123  lgsval2lem  15126  lgsdir2lem4  15147  lgsdir2lem5  15148  lgsdir2  15149  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  2sqlem6  15207  2sqlem10  15212  pwle2  15489  pwf1oexmid  15490  subctctexmid  15491  pw1nct  15493  peano4nninf  15496  nninfalllem1  15498  nninfall  15499  nninfsellemeq  15504  nninfsellemqall  15505  sbthom  15516  refeq  15518  isomninnlem  15520  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  apdiff  15538  iswomninnlem  15539  ismkvnnlem  15542  redcwlpolemeq1  15544  ltlenmkv  15560