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  3623  ifnefals  3671  ifeqeqxdc  3673  intab  3983  exmid01  4316  exmidundif  4324  exmidundifim  4325  frirrg  4476  reg2exmidlema  4661  imadiflem  5440  fvco4  5754  fvmptt  5774  fcoconst  5853  funopsn  5865  f1imass  5953  fcof1  5962  fliftfun  5975  riotass2  6040  ovmpodxf  6187  fsuppeq  6460  fsuppeqg  6461  suppssdc  6473  suppssfvg  6476  dftpos4  6507  tfrlem1  6552  tfrlem3ag  6553  tfrlemibacc  6570  tfrlemibfn  6572  tfrlemi1  6576  tfrlemi14d  6577  tfr1onlem3ag  6581  tfr1onlembacc  6586  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfrcllembacc  6599  tfrcllembfn  6601  tfrcllemaccex  6605  frecabcl  6643  nntr2  6749  dcdifsnid  6750  nnm00  6776  ecopovsymg  6881  ecopoverg  6883  th3qlem1  6884  mapss  6939  f1imaen2g  7046  pw2f1odclem  7100  xpen  7111  xpmapenlem  7115  mapunen  7117  phpm  7133  fidifsnen  7138  dif1enen  7150  fiunsnnn  7151  fin0  7155  fin0or  7156  findcard2d  7161  findcard2sd  7162  diffifi  7164  isinfinf  7167  tridc  7170  fimax2gtrilemstep  7171  fimax2gtri  7172  en2eqpr  7180  onunsnss  7190  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  unfiin  7199  fisseneq  7208  ssfirab  7210  f1finf1o  7230  fidcenumlemrks  7236  fidcenumlemrk  7237  fidcenumlemr  7238  fidcenum  7239  ffsuppbi  7266  2omap  7282  suplub2ti  7305  supisolem  7312  ordiso2  7339  djudom  7397  omp1eomlem  7398  difinfsnlem  7403  difinfinf  7405  ctm  7413  ctssdclemn0  7414  enumct  7419  nnnninfeq  7432  nnnninfeq2  7433  nninfisol  7437  enomnilem  7442  finomni  7444  exmidomni  7446  fodju0  7451  ismkvnex  7459  enmkvlem  7465  enwomnilem  7473  pr2cv1  7505  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  exmidontriimlem1  7541  exmidontriimlem2  7542  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  netap  7584  exmidapne  7590  dfplpq2  7685  dfmpq2  7686  mulpipqqs  7704  nqpi  7709  distrnqg  7718  prarloclemarch  7749  enq0tr  7765  nqnq0pi  7769  nq0nn  7773  nnnq0lem1  7777  prarloclemup  7826  prarloclem3  7828  prarloclemcalc  7833  genplt2i  7841  addnqprllem  7858  addnqprulem  7859  appdivnq  7894  distrlem1prl  7913  distrlem1pru  7914  ltaddpr  7928  ltexprlemlol  7933  ltexprlemupu  7935  ltexprlemdisj  7937  addcanprleml  7945  ltaprlem  7949  addextpr  7952  recexprlemopu  7958  recexprlemdisj  7961  recexprlem1ssl  7964  aptiprleml  7970  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemdisj  7982  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemladdfu  8008  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemexbt  8037  suplocexprlemru  8050  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  prsrlem1  8073  recexgt0sr  8104  mulgt0sr  8109  archsr  8113  caucvgsrlemcau  8124  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  addcnsr  8165  mulcnsr  8166  mulcnsrec  8174  axmulcom  8202  nntopi  8225  axcaucvglemcau  8229  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  mpomulf  8280  axsuploc  8362  ltntri  8418  cnegexlem2  8466  cnegexlem3  8467  addsub4  8533  le2add  8736  lt2add  8737  lt2sub  8752  le2sub  8753  rereim  8878  apreim  8895  mulreim  8896  apcotr  8899  apadd1  8900  addext  8902  mulext1  8904  mulext  8906  apti  8914  aptap  8942  receuap  8963  rec11rap  9005  divdivdivap  9007  divadddivap  9021  divsubdivap  9022  rerecclap  9024  recgt0  9144  prodgt0gt0  9145  prodgt0  9146  prodge0  9148  lemulge11  9160  lt2mul2div  9173  ltrec  9177  lerec  9178  ltrec1  9182  lediv2a  9189  mulle0r  9238  sup3exmid  9251  zdiv  9687  eluzuzle  9883  supinfneg  9948  infsupneg  9949  infregelbex  9951  xrltso  10151  xnn0dcle  10157  xnn0letri  10158  npnflt  10170  nmnfgt  10173  z2ge  10181  xaddf  10199  xaddval  10200  xpncan  10226  xleadd1a  10228  xltadd1  10231  xaddge0  10233  xle2add  10234  xleaddadd  10242  ixxss1  10259  ixxss2  10260  elico2  10292  iccsupr  10321  fzass4  10420  fzrev  10443  fz0fzelfz0  10486  fzocatel  10569  elfzomelpfzo  10601  zsupcllemstep  10614  exbtwnzlemstep  10634  rebtwn2zlemstep  10639  qbtwnxr  10644  xqltnle  10654  apbtwnz  10661  btwnzge0  10687  modqid  10738  modqcyc  10748  modqcyc2  10749  modqaddabs  10751  modqaddmod  10752  mulqaddmodid  10753  modqmuladd  10755  modqltm1p1mod  10765  modqsubmod  10771  modqsubmodmod  10772  modaddmodlo  10777  modqmulmod  10778  modqmulmodr  10779  modqsubdir  10782  addmodlteq  10787  nninfinf  10832  iseqf1olemab  10891  iseqf1olemmo  10894  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  seqf1oglem1  10908  seqf1oglem2  10909  seqf1og  10910  exp3val  10930  expcl2lemap  10940  expap0  10958  expnegzap  10962  expmul  10973  leexp1a  10983  qsqeqor  11039  resq01  11047  expnbnd  11053  nn0ltexp2  11099  nn0opth2  11114  facndiv  11129  faclbnd  11131  bcval5  11153  bcpasc  11156  hashennnuni  11170  hashunlem  11196  hashunsng  11200  hashprg  11201  fiprsshashgt1  11210  hashxp  11219  fimaxq  11222  hashfibc  11235  zfz1isolemiso  11239  zfz1isolem1  11240  seq3coll  11242  iswrdiz  11259  wrdnval  11283  ccatlen  11311  ccatvalfn  11317  ccatsymb  11318  ccatalpha  11329  ccat2s1fstg  11364  swrdclg  11370  swrdsb0eq  11385  pfxwrdsymbg  11410  wrdind  11442  wrd2ind  11443  swrdccatin2  11449  pfxccatin12lem2  11451  pfxccatin12  11453  pfxccat3  11454  swrdccat  11455  shftlem  11529  shftfvalg  11531  shftfval  11534  2shfti  11544  caucvgrelemrec  11692  caucvgrelemcau  11693  caucvgre  11694  cvg1nlemcau  11697  cvg1nlemres  11698  resqrexlemcalc3  11729  resqrexlemcvg  11732  resqrexlemglsq  11735  resqrexlemga  11736  sqrtsq  11757  leabs  11787  absexpzap  11793  abslt  11801  absle  11802  abssubap0  11803  caubnd2  11830  icodiamlt  11893  maxleim  11918  maxabslemval  11921  maxleastlt  11928  rexico  11934  zmaxcl  11937  fimaxre2  11940  minmax  11943  xrmaxleim  11957  xrmaxiflemcl  11958  xrmaxifle  11959  xrmaxiflemlub  11961  xrmaxiflemval  11963  xrmaxleastlt  11969  xrmaxltsup  11971  xrmaxadd  11974  xrminmax  11978  xrbdtri  11989  climuni  12006  climshftlemg  12015  iserex  12052  climcau  12060  climrecvg1n  12061  climcvg1nlem  12062  sumeq2  12072  summodclem3  12094  zsumdc  12098  isumss  12105  fisumss  12106  sumsnf  12123  fsumconst  12168  modfsummod  12172  fsum00  12176  fsumabs  12179  fsumrelem  12185  fsumiun  12191  isumsplit  12205  divcnv  12211  geo2sum  12228  geoisumr  12232  cvgratz  12246  ntrivcvgap  12262  prodeq2  12271  prodmodclem2  12291  prodmodc  12292  zproddc  12293  fprodmul  12305  prodsnf  12306  fprodcl2lem  12319  fprodconst  12334  fprodap0  12335  fprodrec  12343  fprodap0f  12350  fprodle  12354  fprodmodd  12355  tanaddap  12453  zdvdsdc  12526  dvds2ln  12538  fsumdvds  12556  dvdsle  12558  dvdsext  12569  divalglemeunn  12635  divalglemex  12636  divalglemeuneg  12637  bitsfzo  12669  bitsmod  12670  bitsinv1lem  12675  bitsinv1  12676  dvdsbnd  12680  gcdsupex  12681  gcdsupcl  12682  dvdslegcd  12688  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemmain  12722  bezoutlemzz  12726  bezoutlembz  12728  bezoutlembi  12729  bezoutlemle  12732  dfgcd3  12734  bezout  12735  dfgcd2  12738  dvdsmulgcd  12749  bezoutr  12756  uzwodc  12761  nninfctlemfo  12764  lcmval  12788  lcmcllem  12792  lcmneg  12799  ncoprmgcdne1b  12814  isprm2lem  12841  prmind2  12845  dvdsnprmd  12850  isprm5  12867  prmdvdsexp  12873  sqrt2irr  12887  oddpwdclemxy  12894  oddpwdclemdc  12898  nonsq  12932  pceu  13021  pcmul  13027  pc2dvds  13056  pcz  13058  pcprmpw2  13059  dvdsprmpweqle  13063  pcfac  13076  qexpz  13078  prmpwdvds  13081  1arith  13093  mul4sq  13120  4sqexercise2  13125  4sqlemsdc  13126  ballotfilem2  13175  ballotfilemsle  13195  ballotfilemsdom  13202  ballotfilemsima  13206  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemhom  13253  ennnfonelemfun  13255  ennnfonelemf1  13256  ennnfonelemim  13262  exmidunben  13264  ctiunctlemfo  13277  omiunct  13282  ssnnctlemct  13284  isstruct2r  13310  ismgm  13623  issgrp  13669  sgrppropd  13679  sgrpidmndm  13684  mndpropd  13704  issubmnd  13706  resmhm2b  13747  gsumwmhm  13756  isgrpinv  13812  grplmulf1o  13832  dfgrp3mlem  13856  grplactcnv  13860  mhmid  13871  mhmmnd  13872  ghmgrp  13874  mulgval  13878  mulgfng  13880  mulgnnp1  13886  mulgnn0dir  13908  mulgneg2  13912  mhmmulg  13919  grpissubg  13950  isnsg  13958  isnsg3  13963  nmzsubg  13966  ghmmhmb  14010  ghmpreima  14022  ghmnsgpreima  14025  ghmf1  14029  ghmf1o  14031  conjghm  14032  conjnmz  14035  conjnmzb  14036  ghmcmn  14083  gsumfzconst  14097  gfsumz  14112  gfsumcl  14113  prdsval  14118  prdsidlem  14138  pwssub  14161  issrg  14211  srglmhm  14239  srgrmhm  14240  isring  14246  ringadd2  14273  ringlghm  14307  ringrghm  14308  oppr1g  14329  dvdsrvald  14341  dvdsrd  14342  dvdsrex  14346  dvdsrmul1  14350  unitgrp  14364  rhmopp  14424  subrgintm  14492  subrgpropd  14502  isdomn  14519  aprnzr  14540  opprdrng  14561  lmodprop2d  14625  lssvacl  14642  lssvsubcl  14643  lssvscl  14652  lsslss  14658  lss1d  14660  lsspropdg  14708  expghmap  14884  mulgghm2  14885  znunit  14936  znrrg  14937  mplvalcoe  14974  mplsubgfilemcl  14983  mplsubgfileminv  14984  mplsubgfi  14985  opnssneib  15150  restbasg  15162  restopn2  15177  iscnp4  15212  cnss2  15221  cnconst2  15227  cnptopresti  15232  cnptoprest2  15234  neitx  15262  uptx  15268  txrest  15270  txdis1cn  15272  xmetres2  15373  xblss2ps  15398  blhalf  15402  blssps  15421  blss  15422  blssexps  15423  blssex  15424  blin2  15426  metequiv2  15490  bdmetval  15494  metcnp3  15505  metcnp  15506  metcn  15508  metcnpi  15509  metcnpi2  15510  txmetcnp  15512  txmetcn  15513  qtopbas  15516  tgqioo  15549  mpomulcn  15560  fsumcncntop  15561  elcncf2  15568  mulcncflem  15601  mulcncf  15602  suplociccreex  15618  limcdifap  15656  cnplimcim  15661  cnplimccntop  15664  limccnpcntop  15669  dvcj  15703  dvmptfsum  15719  dveflem  15720  ply1termlem  15736  plyaddlem1  15741  plymullem1  15742  plycolemc  15752  plycjlemc  15754  plyrecj  15757  dvply1  15759  reeff1olem  15765  eflt  15769  sin0pilem1  15775  ptolemy  15818  coseq0q4123  15828  coseq0negpitopi  15830  cos02pilt1  15845  cos11  15847  ioocosf1o  15848  rpcxpmul2  15907  cxplt  15910  cxple  15911  cxplt3  15914  apcxp2  15933  rprelogbmul  15949  rprelogbdiv  15951  pellexlem3  15976  dvdsppwf1o  15986  perfect  15998  lgsval  16006  lgsfcl2  16008  lgscllem  16009  lgsval2lem  16012  lgsdir2lem4  16033  lgsdir2lem5  16034  lgsdir2  16035  lgsne0  16040  gausslemma2dlem1a  16060  gausslemma2dlem1f1o  16062  2sqlem6  16122  2sqlem10  16127  umgrnloopv  16238  umgrvad2edg  16335  usgr1eop  16369  wlkvtxiedg  16469  wlkvtxiedgg  16470  upgredginwlk  16480  upgriswlkdc  16484  clwwlkccatlem  16524  eupth2lem3lem4fi  16597  pw1ndom3  16903  pw1map  16908  pwle2  16911  pwf1oexmid  16912  subctctexmid  16913  pw1nct  16916  peano4nninf  16923  nninfalllem1  16925  nninfall  16926  nninfsellemeq  16931  nninfsellemqall  16932  nnnninfex  16939  nninfnfiinf  16940  sbthom  16945  refeq  16947  isomninnlem  16953  trilpolemeq1  16963  trilpolemlt1  16964  trirec0  16967  apdiff  16971  iswomninnlem  16973  ismkvnnlem  16976  redcwlpolemeq1  16978  trimul0or  16984  ltlenmkv  16995