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  7281  exmidfodomrlemrALT  7282  exmidaclem  7291  exmidontriimlem1  7304  exmidontriimlem2  7305  exmidontriimlem3  7306  exmidontriimlem4  7307  exmidontriim  7308  netap  7337  exmidapne  7343  dfplpq2  7438  dfmpq2  7439  mulpipqqs  7457  nqpi  7462  distrnqg  7471  prarloclemarch  7502  enq0tr  7518  nqnq0pi  7522  nq0nn  7526  nnnq0lem1  7530  prarloclemup  7579  prarloclem3  7581  prarloclemcalc  7586  genplt2i  7594  addnqprllem  7611  addnqprulem  7612  appdivnq  7647  distrlem1prl  7666  distrlem1pru  7667  ltaddpr  7681  ltexprlemlol  7686  ltexprlemupu  7688  ltexprlemdisj  7690  addcanprleml  7698  ltaprlem  7702  addextpr  7705  recexprlemopu  7711  recexprlemdisj  7714  recexprlem1ssl  7717  aptiprleml  7723  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemlol  7731  cauappcvgprlemopu  7732  cauappcvgprlemdisj  7735  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemopu  7755  caucvgprlemladdfu  7761  caucvgprprlemml  7778  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemexbt  7790  suplocexprlemru  7803  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  prsrlem1  7826  recexgt0sr  7857  mulgt0sr  7862  archsr  7866  caucvgsrlemcau  7877  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  addcnsr  7918  mulcnsr  7919  mulcnsrec  7927  axmulcom  7955  nntopi  7978  axcaucvglemcau  7982  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  mpomulf  8033  axsuploc  8116  ltntri  8171  cnegexlem2  8219  cnegexlem3  8220  addsub4  8286  le2add  8488  lt2add  8489  lt2sub  8504  le2sub  8505  rereim  8630  apreim  8647  mulreim  8648  apcotr  8651  apadd1  8652  addext  8654  mulext1  8656  mulext  8658  apti  8666  aptap  8694  receuap  8713  rec11rap  8755  divdivdivap  8757  divadddivap  8771  divsubdivap  8772  rerecclap  8774  recgt0  8894  prodgt0gt0  8895  prodgt0  8896  prodge0  8898  lemulge11  8910  lt2mul2div  8923  ltrec  8927  lerec  8928  ltrec1  8932  lediv2a  8939  mulle0r  8988  sup3exmid  9001  zdiv  9431  eluzuzle  9626  supinfneg  9686  infsupneg  9687  infregelbex  9689  xrltso  9888  xnn0dcle  9894  xnn0letri  9895  npnflt  9907  nmnfgt  9910  z2ge  9918  xaddf  9936  xaddval  9937  xpncan  9963  xleadd1a  9965  xltadd1  9968  xaddge0  9970  xle2add  9971  xleaddadd  9979  ixxss1  9996  ixxss2  9997  elico2  10029  iccsupr  10058  fzass4  10154  fzrev  10176  fz0fzelfz0  10219  fzocatel  10292  elfzomelpfzo  10324  zsupcllemstep  10336  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  qbtwnxr  10364  xqltnle  10374  apbtwnz  10381  btwnzge0  10407  modqid  10458  modqcyc  10468  modqcyc2  10469  modqaddabs  10471  modqaddmod  10472  mulqaddmodid  10473  modqmuladd  10475  modqltm1p1mod  10485  modqsubmod  10491  modqsubmodmod  10492  modaddmodlo  10497  modqmulmod  10498  modqmulmodr  10499  modqsubdir  10502  addmodlteq  10507  nninfinf  10552  iseqf1olemab  10611  iseqf1olemmo  10614  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  seqf1oglem1  10628  seqf1oglem2  10629  seqf1og  10630  exp3val  10650  expcl2lemap  10660  expap0  10678  expnegzap  10682  expmul  10693  leexp1a  10703  qsqeqor  10759  expnbnd  10772  nn0ltexp2  10818  nn0opth2  10833  facndiv  10848  faclbnd  10850  bcval5  10872  bcpasc  10875  hashennnuni  10888  hashunlem  10913  hashunsng  10916  hashprg  10917  fiprsshashgt1  10926  hashxp  10935  fimaxq  10936  zfz1isolemiso  10948  zfz1isolem1  10949  seq3coll  10951  iswrdiz  10959  wrdnval  10982  shftlem  10998  shftfvalg  11000  shftfval  11003  2shfti  11013  caucvgrelemrec  11161  caucvgrelemcau  11162  caucvgre  11163  cvg1nlemcau  11166  cvg1nlemres  11167  resqrexlemcalc3  11198  resqrexlemcvg  11201  resqrexlemglsq  11204  resqrexlemga  11205  sqrtsq  11226  leabs  11256  absexpzap  11262  abslt  11270  absle  11271  abssubap0  11272  caubnd2  11299  icodiamlt  11362  maxleim  11387  maxabslemval  11390  maxleastlt  11397  rexico  11403  zmaxcl  11406  fimaxre2  11409  minmax  11412  xrmaxleim  11426  xrmaxiflemcl  11427  xrmaxifle  11428  xrmaxiflemlub  11430  xrmaxiflemval  11432  xrmaxleastlt  11438  xrmaxltsup  11440  xrmaxadd  11443  xrminmax  11447  xrbdtri  11458  climuni  11475  climshftlemg  11484  iserex  11521  climcau  11529  climrecvg1n  11530  climcvg1nlem  11531  sumeq2  11541  summodclem3  11562  zsumdc  11566  isumss  11573  fisumss  11574  sumsnf  11591  fsumconst  11636  modfsummod  11640  fsum00  11644  fsumabs  11647  fsumrelem  11653  fsumiun  11659  isumsplit  11673  divcnv  11679  geo2sum  11696  geoisumr  11700  cvgratz  11714  ntrivcvgap  11730  prodeq2  11739  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodmul  11773  prodsnf  11774  fprodcl2lem  11787  fprodconst  11802  fprodap0  11803  fprodrec  11811  fprodap0f  11818  fprodle  11822  fprodmodd  11823  tanaddap  11921  zdvdsdc  11994  dvds2ln  12006  fsumdvds  12024  dvdsle  12026  dvdsext  12037  divalglemeunn  12103  divalglemex  12104  divalglemeuneg  12105  bitsfzo  12137  bitsmod  12138  bitsinv1lem  12143  bitsinv1  12144  dvdsbnd  12148  gcdsupex  12149  gcdsupcl  12150  dvdslegcd  12156  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemzz  12194  bezoutlembz  12196  bezoutlembi  12197  bezoutlemle  12200  dfgcd3  12202  bezout  12203  dfgcd2  12206  dvdsmulgcd  12217  bezoutr  12224  uzwodc  12229  nninfctlemfo  12232  lcmval  12256  lcmcllem  12260  lcmneg  12267  ncoprmgcdne1b  12282  isprm2lem  12309  prmind2  12313  dvdsnprmd  12318  isprm5  12335  prmdvdsexp  12341  sqrt2irr  12355  oddpwdclemxy  12362  oddpwdclemdc  12366  nonsq  12400  pceu  12489  pcmul  12495  pc2dvds  12524  pcz  12526  pcprmpw2  12527  dvdsprmpweqle  12531  pcfac  12544  qexpz  12546  prmpwdvds  12549  1arith  12561  mul4sq  12588  4sqexercise2  12593  4sqlemsdc  12594  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemhom  12657  ennnfonelemfun  12659  ennnfonelemf1  12660  ennnfonelemim  12666  exmidunben  12668  ctiunctlemfo  12681  omiunct  12686  ssnnctlemct  12688  isstruct2r  12714  prdsval  12975  ismgm  13059  issgrp  13105  sgrppropd  13115  sgrpidmndm  13122  mndpropd  13142  issubmnd  13144  prdsidlem  13149  resmhm2b  13191  gsumwmhm  13200  isgrpinv  13256  grplmulf1o  13276  dfgrp3mlem  13300  grplactcnv  13304  pwssub  13315  mhmid  13321  mhmmnd  13322  ghmgrp  13324  mulgval  13328  mulgfng  13330  mulgnnp1  13336  mulgnn0dir  13358  mulgneg2  13362  mhmmulg  13369  grpissubg  13400  isnsg  13408  isnsg3  13413  nmzsubg  13416  ghmmhmb  13460  ghmpreima  13472  ghmnsgpreima  13475  ghmf1  13479  ghmf1o  13481  conjghm  13482  conjnmz  13485  conjnmzb  13486  ghmcmn  13533  gsumfzconst  13547  issrg  13597  srglmhm  13625  srgrmhm  13626  isring  13632  ringadd2  13659  ringlghm  13693  ringrghm  13694  oppr1g  13714  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrd  13726  dvdsrex  13730  dvdsrmul1  13734  unitgrp  13748  rhmopp  13808  subrgintm  13875  subrgpropd  13885  isdomn  13901  lmodprop2d  13980  lssvacl  13997  lssvsubcl  13998  lssvscl  14007  lsslss  14013  lss1d  14015  lsspropdg  14063  expghmap  14239  mulgghm2  14240  znunit  14291  znrrg  14292  opnssneib  14476  restbasg  14488  restopn2  14503  iscnp4  14538  cnss2  14547  cnconst2  14553  cnptopresti  14558  cnptoprest2  14560  neitx  14588  uptx  14594  txrest  14596  txdis1cn  14598  xmetres2  14699  xblss2ps  14724  blhalf  14728  blssps  14747  blss  14748  blssexps  14749  blssex  14750  blin2  14752  metequiv2  14816  bdmetval  14820  metcnp3  14831  metcnp  14832  metcn  14834  metcnpi  14835  metcnpi2  14836  txmetcnp  14838  txmetcn  14839  qtopbas  14842  tgqioo  14875  mpomulcn  14886  fsumcncntop  14887  elcncf2  14894  mulcncflem  14927  mulcncf  14928  suplociccreex  14944  limcdifap  14982  cnplimcim  14987  cnplimccntop  14990  limccnpcntop  14995  dvcj  15029  dvmptfsum  15045  dveflem  15046  ply1termlem  15062  plyaddlem1  15067  plymullem1  15068  plycolemc  15078  plycjlemc  15080  plyrecj  15083  dvply1  15085  reeff1olem  15091  eflt  15095  sin0pilem1  15101  ptolemy  15144  coseq0q4123  15154  coseq0negpitopi  15156  cos02pilt1  15171  cos11  15173  ioocosf1o  15174  rpcxpmul2  15233  cxplt  15236  cxple  15237  cxplt3  15240  apcxp2  15259  rprelogbmul  15275  rprelogbdiv  15277  dvdsppwf1o  15309  perfect  15321  lgsval  15329  lgsfcl2  15331  lgscllem  15332  lgsval2lem  15335  lgsdir2lem4  15356  lgsdir2lem5  15357  lgsdir2  15358  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  2sqlem6  15445  2sqlem10  15450  2omap  15726  pwle2  15729  pwf1oexmid  15730  subctctexmid  15731  pw1nct  15734  peano4nninf  15737  nninfalllem1  15739  nninfall  15740  nninfsellemeq  15745  nninfsellemqall  15746  sbthom  15757  refeq  15759  isomninnlem  15761  trilpolemeq1  15771  trilpolemlt1  15772  trirec0  15775  apdiff  15779  iswomninnlem  15780  ismkvnnlem  15783  redcwlpolemeq1  15785  ltlenmkv  15801