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 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp1lr  1092  simp2lr  1096  simp3lr  1100  bilukdc  1445  dcun  3637  ifnefals  3685  ifeqeqxdc  3687  intab  3999  exmid01  4335  exmidundif  4343  exmidundifim  4344  frirrg  4495  reg2exmidlema  4681  imadiflem  5460  relndmfv  5728  fvco4  5777  fvmptt  5797  fcoconst  5879  funopsn  5891  f1imass  5980  fcof1  5989  fliftfun  6002  riotass2  6067  ovmpodxf  6214  fsuppeq  6487  fsuppeqg  6488  suppssdc  6500  suppssfvg  6503  dftpos4  6534  tfrlem1  6579  tfrlem3ag  6580  tfrlemibacc  6597  tfrlemibfn  6599  tfrlemi1  6603  tfrlemi14d  6604  tfr1onlem3ag  6608  tfr1onlembacc  6613  tfr1onlembfn  6615  tfr1onlemaccex  6619  tfrcllembacc  6626  tfrcllembfn  6628  tfrcllemaccex  6632  frecabcl  6670  nntr2  6776  dcdifsnid  6777  nnm00  6803  ecopovsymg  6908  ecopoverg  6910  th3qlem1  6911  mapss  6973  f1imaen2g  7080  pw2f1odclem  7134  xpen  7145  xpmapenlem  7149  mapunen  7151  phpm  7167  fidifsnen  7172  dif1enen  7184  fiunsnnn  7185  fin0  7189  fin0or  7190  findcard2d  7195  findcard2sd  7196  diffifi  7198  isinfinf  7201  tridc  7204  fimax2gtrilemstep  7205  fimax2gtri  7206  en2eqpr  7214  onunsnss  7224  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  unfiin  7233  fisseneq  7242  ssfirab  7244  f1finf1o  7264  fidcenumlemrks  7270  fidcenumlemrk  7271  fidcenumlemr  7272  fidcenum  7273  ffsuppbi  7300  fdcf1  7316  f1setfi  7317  2omap  7318  suplub2ti  7341  supisolem  7348  ordiso2  7375  djudom  7433  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctm  7449  ctssdclemn0  7450  enumct  7455  nnnninfeq  7468  nnnninfeq2  7469  nninfisol  7473  enomnilem  7478  finomni  7480  exmidomni  7482  fodju0  7487  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  pr2cv1  7541  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem1  7577  exmidontriimlem2  7578  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  netap  7620  exmidapne  7626  dfplpq2  7721  dfmpq2  7722  mulpipqqs  7740  nqpi  7745  distrnqg  7754  prarloclemarch  7785  enq0tr  7801  nqnq0pi  7805  nq0nn  7809  nnnq0lem1  7813  prarloclemup  7862  prarloclem3  7864  prarloclemcalc  7869  genplt2i  7877  addnqprllem  7894  addnqprulem  7895  appdivnq  7930  distrlem1prl  7949  distrlem1pru  7950  ltaddpr  7964  ltexprlemlol  7969  ltexprlemupu  7971  ltexprlemdisj  7973  addcanprleml  7981  ltaprlem  7985  addextpr  7988  recexprlemopu  7994  recexprlemdisj  7997  recexprlem1ssl  8000  aptiprleml  8006  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemdisj  8018  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemladdfu  8044  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  prsrlem1  8109  recexgt0sr  8140  mulgt0sr  8145  archsr  8149  caucvgsrlemcau  8160  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  addcnsr  8201  mulcnsr  8202  mulcnsrec  8210  axmulcom  8238  nntopi  8261  axcaucvglemcau  8265  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  mpomulf  8316  axsuploc  8398  ltntri  8454  cnegexlem2  8502  cnegexlem3  8503  addsub4  8569  le2add  8772  lt2add  8773  lt2sub  8788  le2sub  8789  rereim  8915  apreim  8932  mulreim  8933  apcotr  8936  apadd1  8937  addext  8939  mulext1  8941  mulext  8943  apti  8951  aptap  8979  receuap  9000  rec11rap  9042  divdivdivap  9044  divadddivap  9058  divsubdivap  9059  rerecclap  9061  recgt0  9181  prodgt0gt0  9182  prodgt0  9183  prodge0  9185  lemulge11  9197  lt2mul2div  9210  ltrec  9214  lerec  9215  ltrec1  9219  lediv2a  9226  mulle0r  9275  sup3exmid  9288  zdiv  9736  eluzuzle  9932  supinfneg  9997  infsupneg  9998  infregelbex  10000  xrltso  10200  xnn0dcle  10206  xnn0letri  10207  npnflt  10219  nmnfgt  10222  z2ge  10230  xaddf  10248  xaddval  10249  xpncan  10275  xleadd1a  10277  xltadd1  10280  xaddge0  10282  xle2add  10283  xleaddadd  10291  ixxss1  10308  ixxss2  10309  elico2  10341  iccsupr  10370  fzass4  10470  fzrev  10493  fz0fzelfz0  10536  fzocatel  10619  elfzomelpfzo  10651  zsupcllemstep  10664  exbtwnzlemstep  10684  rebtwn2zlemstep  10689  qbtwnxr  10694  xqltnle  10704  apbtwnz  10711  btwnzge0  10737  modqid  10788  modqcyc  10798  modqcyc2  10799  modqaddabs  10801  modqaddmod  10802  mulqaddmodid  10803  modqmuladd  10805  modqltm1p1mod  10815  modqsubmod  10821  modqsubmodmod  10822  modaddmodlo  10827  modqmulmod  10828  modqmulmodr  10829  modqsubdir  10832  addmodlteq  10837  nninfinf  10882  iseqf1olemab  10941  iseqf1olemmo  10944  iseqf1olemjpcl  10947  iseqf1olemqpcl  10948  seqf1oglem1  10958  seqf1oglem2  10959  seqf1og  10960  exp3val  10980  expcl2lemap  10990  expap0  11008  expnegzap  11012  expmul  11023  leexp1a  11033  qsqeqor  11089  resq01  11097  expnbnd  11103  nn0ltexp2  11149  nn0opth2  11164  facndiv  11179  faclbnd  11181  bcval5  11203  bcpasc  11206  hashennnuni  11220  hashunlem  11246  hashunsng  11250  hashprg  11251  fiprsshashgt1  11260  hashxp  11269  fimaxq  11272  hashfibc  11285  zfz1isolemiso  11293  zfz1isolem1  11294  seq3coll  11296  iswrdiz  11313  wrdnval  11337  ccatlen  11365  ccatvalfn  11371  ccatsymb  11372  ccatalpha  11383  ccat2s1fstg  11418  swrdclg  11424  swrdsb0eq  11439  pfxwrdsymbg  11464  wrdind  11496  wrd2ind  11497  swrdccatin2  11503  pfxccatin12lem2  11505  pfxccatin12  11507  pfxccat3  11508  swrdccat  11509  shftlem  11583  shftfvalg  11585  shftfval  11588  2shfti  11598  caucvgrelemrec  11747  caucvgrelemcau  11748  caucvgre  11749  cvg1nlemcau  11752  cvg1nlemres  11753  resqrexlemcalc3  11784  resqrexlemcvg  11787  resqrexlemglsq  11790  resqrexlemga  11791  sqrtsq  11812  leabs  11842  absexpzap  11848  abslt  11856  absle  11857  abssubap0  11858  caubnd2  11885  icodiamlt  11948  maxleim  11973  maxabslemval  11976  maxleastlt  11983  rexico  11989  zmaxcl  11992  fimaxre2  11995  minmax  11998  xrmaxleim  12012  xrmaxiflemcl  12013  xrmaxifle  12014  xrmaxiflemlub  12016  xrmaxiflemval  12018  xrmaxleastlt  12024  xrmaxltsup  12026  xrmaxadd  12029  xrminmax  12033  xrbdtri  12044  climuni  12061  climshftlemg  12070  iserex  12107  climcau  12115  climrecvg1n  12116  climcvg1nlem  12117  sumeq2  12127  summodclem3  12149  zsumdc  12153  isumss  12160  fisumss  12161  sumsnf  12178  fsumconst  12223  modfsummod  12227  fsum00  12231  fsumabs  12234  fsumrelem  12240  fsumiun  12246  isumsplit  12260  divcnv  12266  geo2sum  12283  geoisumr  12287  cvgratz  12301  ntrivcvgap  12317  prodeq2  12326  prodmodclem2  12346  prodmodc  12347  zproddc  12348  fprodmul  12360  prodsnf  12361  fprodcl2lem  12374  fprodconst  12389  fprodap0  12390  fprodrec  12398  fprodap0f  12405  fprodle  12409  fprodmodd  12410  tanaddap  12508  zdvdsdc  12581  dvds2ln  12593  fsumdvds  12611  dvdsle  12613  dvdsext  12624  divalglemeunn  12690  divalglemex  12691  divalglemeuneg  12692  bitsfzo  12724  bitsmod  12725  bitsinv1lem  12730  bitsinv1  12731  dvdsbnd  12735  gcdsupex  12736  gcdsupcl  12737  dvdslegcd  12743  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlemzz  12781  bezoutlembz  12783  bezoutlembi  12784  bezoutlemle  12787  dfgcd3  12789  bezout  12790  dfgcd2  12793  dvdsmulgcd  12804  bezoutr  12811  uzwodc  12816  nninfctlemfo  12819  lcmval  12843  lcmcllem  12847  lcmneg  12854  ncoprmgcdne1b  12869  isprm2lem  12896  prmind2  12900  dvdsnprmd  12905  isprm5  12922  prmdvdsexp  12928  sqrt2irr  12942  oddpwdclemxy  12949  oddpwdclemdc  12953  nonsq  12987  pceu  13076  pcmul  13082  pc2dvds  13111  pcz  13113  pcprmpw2  13114  dvdsprmpweqle  13118  pcfac  13131  qexpz  13133  prmpwdvds  13136  1arith  13148  mul4sq  13175  4sqexercise2  13180  4sqlemsdc  13181  ballotfilem2  13230  ballotfilemsle  13250  ballotfilemsdom  13257  ballotfilemsima  13261  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemhom  13308  ennnfonelemfun  13310  ennnfonelemf1  13311  ennnfonelemim  13317  exmidunben  13319  ctiunctlemfo  13332  omiunct  13337  ssnnctlemct  13339  isstruct2r  13365  ismgm  13679  issgrp  13720  sgrppropd  13730  sgrpidmndm  13735  mndpropd  13755  issubmnd  13757  resmhm2b  13798  gzsumwmhm  13805  isgrpinv  13861  grplmulf1o  13881  dfgrp3mlem  13905  grplactcnv  13909  mhmid  13920  mhmmnd  13921  ghmgrp  13923  mulgval  13927  mulgfng  13929  mulgnnp1  13935  mulgnn0dir  13957  mulgneg2  13961  mhmmulg  13968  grpissubg  13999  isnsg  14007  isnsg3  14012  nmzsubg  14015  ghmmhmb  14059  ghmpreima  14071  ghmnsgpreima  14074  ghmf1  14078  ghmf1o  14080  conjghm  14081  conjnmz  14084  conjnmzb  14085  ghmcmn  14133  gzsumconst  14145  gsumzfi  14160  gsumclfi  14161  gsummptfidmadd  14163  gsumsubmclfi  14165  gsumconstcmn  14168  prdsval  14175  prdsidlem  14195  pwssub  14218  issrg  14271  srglmhm  14299  srgrmhm  14300  isring  14306  ringadd2  14334  ringlghm  14368  ringrghm  14369  oppr1g  14390  dvdsrvald  14402  dvdsrd  14403  dvdsrex  14407  dvdsrmul1  14411  unitgrp  14425  rhmopp  14485  subrgintm  14553  subrgpropd  14563  isdomn  14580  aprnzr  14601  opprdrng  14622  lmodprop2d  14687  lssvacl  14704  lssvsubcl  14705  lssvscl  14714  lsslss  14720  lss1d  14722  lsspropdg  14770  gsumfsum  14925  expghmap  14944  mulgghm2  14945  znunit  14996  znrrg  14997  issubassa2  15037  assamulgscmlem1  15043  assamulgscmlem2  15044  mplvalcoe  15083  mplsubgfilemcl  15092  mplsubgfileminv  15093  mplsubgfi  15094  opnssneib  15259  restbasg  15271  restopn2  15286  iscnp4  15321  cnss2  15330  cnconst2  15336  cnptopresti  15341  cnptoprest2  15343  neitx  15371  uptx  15377  txrest  15379  txdis1cn  15381  xmetres2  15482  xblss2ps  15507  blhalf  15511  blssps  15530  blss  15531  blssexps  15532  blssex  15533  blin2  15535  metequiv2  15599  bdmetval  15603  metcnp3  15614  metcnp  15615  metcn  15617  metcnpi  15618  metcnpi2  15619  txmetcnp  15621  txmetcn  15622  qtopbas  15625  tgqioo  15658  mpomulcn  15669  fsumcncntop  15670  elcncf2  15677  mulcncflem  15710  mulcncf  15711  suplociccreex  15727  limcdifap  15765  cnplimcim  15770  cnplimccntop  15773  limccnpcntop  15778  dvcj  15812  dvmptfsum  15828  dveflem  15829  ply1termlem  15845  plyaddlem1  15850  plymullem1  15851  plycolemc  15861  plycjlemc  15863  plyrecj  15866  dvply1  15868  reeff1olem  15874  eflt  15878  sin0pilem1  15885  ptolemy  15928  coseq0q4123  15938  coseq0negpitopi  15940  cos02pilt1  15955  cos11  15957  ioocosf1o  15958  logdivlt  15999  logdivle  16000  rpcxpmul2  16021  cxplt  16024  cxple  16025  cxplt3  16028  apcxp2  16047  rprelogbmul  16063  rprelogbdiv  16065  birthdaylem3  16095  pellexlem3  16099  dvdsppwf1o  16109  perfect  16121  bcmax  16125  lgsval  16135  lgsfcl2  16137  lgscllem  16138  lgsval2lem  16141  lgsdir2lem4  16162  lgsdir2lem5  16163  lgsdir2  16164  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  2sqlem6  16251  2sqlem10  16256  umgrnloopv  16367  umgrvad2edg  16464  usgr1eop  16498  wlkvtxiedg  16598  wlkvtxiedgg  16599  upgredginwlk  16609  upgriswlkdc  16613  clwwlkccatlem  16653  eupth2lem3lem4fi  16726  pw1ndom3  17032  pw1map  17037  pwle2  17040  pwf1oexmid  17041  subctctexmid  17042  pw1nct  17045  stnot  17051  peano4nninf  17061  nninfalllem1  17063  nninfall  17064  nninfsellemeq  17069  nninfsellemqall  17070  nnnninfex  17077  nninfnfiinf  17078  sbthom  17083  refeq  17085  isomninnlem  17091  trilpolemeq1  17101  trilpolemlt1  17102  trirec0  17105  apdiff  17109  iswomninnlem  17111  ismkvnnlem  17114  redcwlpolemeq1  17116  ltlenmkv  17132