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  3561  ifnefals  3604  intab  3904  exmid01  4232  exmidundif  4240  exmidundifim  4241  frirrg  4386  reg2exmidlema  4571  imadiflem  5338  fvco4  5636  fvmptt  5656  fcoconst  5736  f1imass  5824  fcof1  5833  fliftfun  5846  riotass2  5907  ovmpodxf  6052  dftpos4  6330  tfrlem1  6375  tfrlem3ag  6376  tfrlemibacc  6393  tfrlemibfn  6395  tfrlemi1  6399  tfrlemi14d  6400  tfr1onlem3ag  6404  tfr1onlembacc  6409  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfrcllembacc  6422  tfrcllembfn  6424  tfrcllemaccex  6428  frecabcl  6466  nntr2  6570  dcdifsnid  6571  nnm00  6597  ecopovsymg  6702  ecopoverg  6704  th3qlem1  6705  mapss  6759  f1imaen2g  6861  pw2f1odclem  6904  xpen  6915  xpmapenlem  6919  phpm  6935  fidifsnen  6940  dif1enen  6950  fiunsnnn  6951  fin0  6955  fin0or  6956  findcard2d  6961  findcard2sd  6962  diffifi  6964  isinfinf  6967  tridc  6969  fimax2gtrilemstep  6970  fimax2gtri  6971  en2eqpr  6977  onunsnss  6987  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  unfiin  6996  fisseneq  7004  ssfirab  7006  f1finf1o  7022  fidcenumlemrks  7028  fidcenumlemrk  7029  fidcenumlemr  7030  fidcenum  7031  suplub2ti  7076  supisolem  7083  ordiso2  7110  djudom  7168  omp1eomlem  7169  difinfsnlem  7174  difinfinf  7176  ctm  7184  ctssdclemn0  7185  enumct  7190  nnnninfeq  7203  nnnninfeq2  7204  nninfisol  7208  enomnilem  7213  finomni  7215  exmidomni  7217  fodju0  7222  ismkvnex  7230  enmkvlem  7236  enwomnilem  7244  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  exmidontriimlem1  7306  exmidontriimlem2  7307  exmidontriimlem3  7308  exmidontriimlem4  7309  exmidontriim  7310  netap  7339  exmidapne  7345  dfplpq2  7440  dfmpq2  7441  mulpipqqs  7459  nqpi  7464  distrnqg  7473  prarloclemarch  7504  enq0tr  7520  nqnq0pi  7524  nq0nn  7528  nnnq0lem1  7532  prarloclemup  7581  prarloclem3  7583  prarloclemcalc  7588  genplt2i  7596  addnqprllem  7613  addnqprulem  7614  appdivnq  7649  distrlem1prl  7668  distrlem1pru  7669  ltaddpr  7683  ltexprlemlol  7688  ltexprlemupu  7690  ltexprlemdisj  7692  addcanprleml  7700  ltaprlem  7704  addextpr  7707  recexprlemopu  7713  recexprlemdisj  7716  recexprlem1ssl  7719  aptiprleml  7725  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemdisj  7737  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemladdfu  7763  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemexbt  7792  suplocexprlemru  7805  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  prsrlem1  7828  recexgt0sr  7859  mulgt0sr  7864  archsr  7868  caucvgsrlemcau  7879  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  suplocsrlemb  7892  suplocsrlempr  7893  suplocsrlem  7894  addcnsr  7920  mulcnsr  7921  mulcnsrec  7929  axmulcom  7957  nntopi  7980  axcaucvglemcau  7984  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  mpomulf  8035  axsuploc  8118  ltntri  8173  cnegexlem2  8221  cnegexlem3  8222  addsub4  8288  le2add  8490  lt2add  8491  lt2sub  8506  le2sub  8507  rereim  8632  apreim  8649  mulreim  8650  apcotr  8653  apadd1  8654  addext  8656  mulext1  8658  mulext  8660  apti  8668  aptap  8696  receuap  8715  rec11rap  8757  divdivdivap  8759  divadddivap  8773  divsubdivap  8774  rerecclap  8776  recgt0  8896  prodgt0gt0  8897  prodgt0  8898  prodge0  8900  lemulge11  8912  lt2mul2div  8925  ltrec  8929  lerec  8930  ltrec1  8934  lediv2a  8941  mulle0r  8990  sup3exmid  9003  zdiv  9433  eluzuzle  9628  supinfneg  9688  infsupneg  9689  infregelbex  9691  xrltso  9890  xnn0dcle  9896  xnn0letri  9897  npnflt  9909  nmnfgt  9912  z2ge  9920  xaddf  9938  xaddval  9939  xpncan  9965  xleadd1a  9967  xltadd1  9970  xaddge0  9972  xle2add  9973  xleaddadd  9981  ixxss1  9998  ixxss2  9999  elico2  10031  iccsupr  10060  fzass4  10156  fzrev  10178  fz0fzelfz0  10221  fzocatel  10294  elfzomelpfzo  10326  zsupcllemstep  10338  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  qbtwnxr  10366  xqltnle  10376  apbtwnz  10383  btwnzge0  10409  modqid  10460  modqcyc  10470  modqcyc2  10471  modqaddabs  10473  modqaddmod  10474  mulqaddmodid  10475  modqmuladd  10477  modqltm1p1mod  10487  modqsubmod  10493  modqsubmodmod  10494  modaddmodlo  10499  modqmulmod  10500  modqmulmodr  10501  modqsubdir  10504  addmodlteq  10509  nninfinf  10554  iseqf1olemab  10613  iseqf1olemmo  10616  iseqf1olemjpcl  10619  iseqf1olemqpcl  10620  seqf1oglem1  10630  seqf1oglem2  10631  seqf1og  10632  exp3val  10652  expcl2lemap  10662  expap0  10680  expnegzap  10684  expmul  10695  leexp1a  10705  qsqeqor  10761  expnbnd  10774  nn0ltexp2  10820  nn0opth2  10835  facndiv  10850  faclbnd  10852  bcval5  10874  bcpasc  10877  hashennnuni  10890  hashunlem  10915  hashunsng  10918  hashprg  10919  fiprsshashgt1  10928  hashxp  10937  fimaxq  10938  zfz1isolemiso  10950  zfz1isolem1  10951  seq3coll  10953  iswrdiz  10961  wrdnval  10984  shftlem  11000  shftfvalg  11002  shftfval  11005  2shfti  11015  caucvgrelemrec  11163  caucvgrelemcau  11164  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemcalc3  11200  resqrexlemcvg  11203  resqrexlemglsq  11206  resqrexlemga  11207  sqrtsq  11228  leabs  11258  absexpzap  11264  abslt  11272  absle  11273  abssubap0  11274  caubnd2  11301  icodiamlt  11364  maxleim  11389  maxabslemval  11392  maxleastlt  11399  rexico  11405  zmaxcl  11408  fimaxre2  11411  minmax  11414  xrmaxleim  11428  xrmaxiflemcl  11429  xrmaxifle  11430  xrmaxiflemlub  11432  xrmaxiflemval  11434  xrmaxleastlt  11440  xrmaxltsup  11442  xrmaxadd  11445  xrminmax  11449  xrbdtri  11460  climuni  11477  climshftlemg  11486  iserex  11523  climcau  11531  climrecvg1n  11532  climcvg1nlem  11533  sumeq2  11543  summodclem3  11564  zsumdc  11568  isumss  11575  fisumss  11576  sumsnf  11593  fsumconst  11638  modfsummod  11642  fsum00  11646  fsumabs  11649  fsumrelem  11655  fsumiun  11661  isumsplit  11675  divcnv  11681  geo2sum  11698  geoisumr  11702  cvgratz  11716  ntrivcvgap  11732  prodeq2  11741  prodmodclem2  11761  prodmodc  11762  zproddc  11763  fprodmul  11775  prodsnf  11776  fprodcl2lem  11789  fprodconst  11804  fprodap0  11805  fprodrec  11813  fprodap0f  11820  fprodle  11824  fprodmodd  11825  tanaddap  11923  zdvdsdc  11996  dvds2ln  12008  fsumdvds  12026  dvdsle  12028  dvdsext  12039  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  bitsfzo  12139  bitsmod  12140  bitsinv1lem  12145  bitsinv1  12146  dvdsbnd  12150  gcdsupex  12151  gcdsupcl  12152  dvdslegcd  12158  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlemzz  12196  bezoutlembz  12198  bezoutlembi  12199  bezoutlemle  12202  dfgcd3  12204  bezout  12205  dfgcd2  12208  dvdsmulgcd  12219  bezoutr  12226  uzwodc  12231  nninfctlemfo  12234  lcmval  12258  lcmcllem  12262  lcmneg  12269  ncoprmgcdne1b  12284  isprm2lem  12311  prmind2  12315  dvdsnprmd  12320  isprm5  12337  prmdvdsexp  12343  sqrt2irr  12357  oddpwdclemxy  12364  oddpwdclemdc  12368  nonsq  12402  pceu  12491  pcmul  12497  pc2dvds  12526  pcz  12528  pcprmpw2  12529  dvdsprmpweqle  12533  pcfac  12546  qexpz  12548  prmpwdvds  12551  1arith  12563  mul4sq  12590  4sqexercise2  12595  4sqlemsdc  12596  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemhom  12659  ennnfonelemfun  12661  ennnfonelemf1  12662  ennnfonelemim  12668  exmidunben  12670  ctiunctlemfo  12683  omiunct  12688  ssnnctlemct  12690  isstruct2r  12716  prdsval  12977  ismgm  13061  issgrp  13107  sgrppropd  13117  sgrpidmndm  13124  mndpropd  13144  issubmnd  13146  prdsidlem  13151  resmhm2b  13193  gsumwmhm  13202  isgrpinv  13258  grplmulf1o  13278  dfgrp3mlem  13302  grplactcnv  13306  pwssub  13317  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgval  13330  mulgfng  13332  mulgnnp1  13338  mulgnn0dir  13360  mulgneg2  13364  mhmmulg  13371  grpissubg  13402  isnsg  13410  isnsg3  13415  nmzsubg  13418  ghmmhmb  13462  ghmpreima  13474  ghmnsgpreima  13477  ghmf1  13481  ghmf1o  13483  conjghm  13484  conjnmz  13487  conjnmzb  13488  ghmcmn  13535  gsumfzconst  13549  issrg  13599  srglmhm  13627  srgrmhm  13628  isring  13634  ringadd2  13661  ringlghm  13695  ringrghm  13696  oppr1g  13716  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrd  13728  dvdsrex  13732  dvdsrmul1  13736  unitgrp  13750  rhmopp  13810  subrgintm  13877  subrgpropd  13887  isdomn  13903  lmodprop2d  13982  lssvacl  13999  lssvsubcl  14000  lssvscl  14009  lsslss  14015  lss1d  14017  lsspropdg  14065  expghmap  14241  mulgghm2  14242  znunit  14293  znrrg  14294  opnssneib  14478  restbasg  14490  restopn2  14505  iscnp4  14540  cnss2  14549  cnconst2  14555  cnptopresti  14560  cnptoprest2  14562  neitx  14590  uptx  14596  txrest  14598  txdis1cn  14600  xmetres2  14701  xblss2ps  14726  blhalf  14730  blssps  14749  blss  14750  blssexps  14751  blssex  14752  blin2  14754  metequiv2  14818  bdmetval  14822  metcnp3  14833  metcnp  14834  metcn  14836  metcnpi  14837  metcnpi2  14838  txmetcnp  14840  txmetcn  14841  qtopbas  14844  tgqioo  14877  mpomulcn  14888  fsumcncntop  14889  elcncf2  14896  mulcncflem  14929  mulcncf  14930  suplociccreex  14946  limcdifap  14984  cnplimcim  14989  cnplimccntop  14992  limccnpcntop  14997  dvcj  15031  dvmptfsum  15047  dveflem  15048  ply1termlem  15064  plyaddlem1  15069  plymullem1  15070  plycolemc  15080  plycjlemc  15082  plyrecj  15085  dvply1  15087  reeff1olem  15093  eflt  15097  sin0pilem1  15103  ptolemy  15146  coseq0q4123  15156  coseq0negpitopi  15158  cos02pilt1  15173  cos11  15175  ioocosf1o  15176  rpcxpmul2  15235  cxplt  15238  cxple  15239  cxplt3  15242  apcxp2  15261  rprelogbmul  15277  rprelogbdiv  15279  dvdsppwf1o  15311  perfect  15323  lgsval  15331  lgsfcl2  15333  lgscllem  15334  lgsval2lem  15337  lgsdir2lem4  15358  lgsdir2lem5  15359  lgsdir2  15360  lgsne0  15365  gausslemma2dlem1a  15385  gausslemma2dlem1f1o  15387  2sqlem6  15447  2sqlem10  15452  2omap  15728  pwle2  15731  pwf1oexmid  15732  subctctexmid  15733  pw1nct  15736  peano4nninf  15739  nninfalllem1  15741  nninfall  15742  nninfsellemeq  15747  nninfsellemqall  15748  nnnninfex  15755  nninfnfiinf  15756  sbthom  15761  refeq  15763  isomninnlem  15765  trilpolemeq1  15775  trilpolemlt1  15776  trirec0  15779  apdiff  15783  iswomninnlem  15784  ismkvnnlem  15787  redcwlpolemeq1  15789  ltlenmkv  15805