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  1087  simp2lr  1091  simp3lr  1095  bilukdc  1440  dcun  3604  ifnefals  3650  intab  3957  exmid01  4288  exmidundif  4296  exmidundifim  4297  frirrg  4447  reg2exmidlema  4632  imadiflem  5409  fvco4  5718  fvmptt  5738  fcoconst  5818  funopsn  5830  f1imass  5915  fcof1  5924  fliftfun  5937  riotass2  6000  ovmpodxf  6147  dftpos4  6429  tfrlem1  6474  tfrlem3ag  6475  tfrlemibacc  6492  tfrlemibfn  6494  tfrlemi1  6498  tfrlemi14d  6499  tfr1onlem3ag  6503  tfr1onlembacc  6508  tfr1onlembfn  6510  tfr1onlemaccex  6514  tfrcllembacc  6521  tfrcllembfn  6523  tfrcllemaccex  6527  frecabcl  6565  nntr2  6671  dcdifsnid  6672  nnm00  6698  ecopovsymg  6803  ecopoverg  6805  th3qlem1  6806  mapss  6860  f1imaen2g  6967  pw2f1odclem  7020  xpen  7031  xpmapenlem  7035  phpm  7052  fidifsnen  7057  dif1enen  7069  fiunsnnn  7070  fin0  7074  fin0or  7075  findcard2d  7080  findcard2sd  7081  diffifi  7083  isinfinf  7086  tridc  7089  fimax2gtrilemstep  7090  fimax2gtri  7091  en2eqpr  7099  onunsnss  7109  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  unfiin  7118  fisseneq  7127  ssfirab  7129  f1finf1o  7146  fidcenumlemrks  7152  fidcenumlemrk  7153  fidcenumlemr  7154  fidcenum  7155  suplub2ti  7200  supisolem  7207  ordiso2  7234  djudom  7292  omp1eomlem  7293  difinfsnlem  7298  difinfinf  7300  ctm  7308  ctssdclemn0  7309  enumct  7314  nnnninfeq  7327  nnnninfeq2  7328  nninfisol  7332  enomnilem  7337  finomni  7339  exmidomni  7341  fodju0  7346  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  pr2cv1  7400  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem1  7436  exmidontriimlem2  7437  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  netap  7473  exmidapne  7479  dfplpq2  7574  dfmpq2  7575  mulpipqqs  7593  nqpi  7598  distrnqg  7607  prarloclemarch  7638  enq0tr  7654  nqnq0pi  7658  nq0nn  7662  nnnq0lem1  7666  prarloclemup  7715  prarloclem3  7717  prarloclemcalc  7722  genplt2i  7730  addnqprllem  7747  addnqprulem  7748  appdivnq  7783  distrlem1prl  7802  distrlem1pru  7803  ltaddpr  7817  ltexprlemlol  7822  ltexprlemupu  7824  ltexprlemdisj  7826  addcanprleml  7834  ltaprlem  7838  addextpr  7841  recexprlemopu  7847  recexprlemdisj  7850  recexprlem1ssl  7853  aptiprleml  7859  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemdisj  7871  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemladdfu  7897  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  prsrlem1  7962  recexgt0sr  7993  mulgt0sr  7998  archsr  8002  caucvgsrlemcau  8013  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  addcnsr  8054  mulcnsr  8055  mulcnsrec  8063  axmulcom  8091  nntopi  8114  axcaucvglemcau  8118  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  mpomulf  8169  axsuploc  8252  ltntri  8307  cnegexlem2  8355  cnegexlem3  8356  addsub4  8422  le2add  8624  lt2add  8625  lt2sub  8640  le2sub  8641  rereim  8766  apreim  8783  mulreim  8784  apcotr  8787  apadd1  8788  addext  8790  mulext1  8792  mulext  8794  apti  8802  aptap  8830  receuap  8849  rec11rap  8891  divdivdivap  8893  divadddivap  8907  divsubdivap  8908  rerecclap  8910  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemulge11  9046  lt2mul2div  9059  ltrec  9063  lerec  9064  ltrec1  9068  lediv2a  9075  mulle0r  9124  sup3exmid  9137  zdiv  9568  eluzuzle  9764  supinfneg  9829  infsupneg  9830  infregelbex  9832  xrltso  10031  xnn0dcle  10037  xnn0letri  10038  npnflt  10050  nmnfgt  10053  z2ge  10061  xaddf  10079  xaddval  10080  xpncan  10106  xleadd1a  10108  xltadd1  10111  xaddge0  10113  xle2add  10114  xleaddadd  10122  ixxss1  10139  ixxss2  10140  elico2  10172  iccsupr  10201  fzass4  10297  fzrev  10319  fz0fzelfz0  10362  fzocatel  10445  elfzomelpfzo  10477  zsupcllemstep  10490  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  qbtwnxr  10518  xqltnle  10528  apbtwnz  10535  btwnzge0  10561  modqid  10612  modqcyc  10622  modqcyc2  10623  modqaddabs  10625  modqaddmod  10626  mulqaddmodid  10627  modqmuladd  10629  modqltm1p1mod  10639  modqsubmod  10645  modqsubmodmod  10646  modaddmodlo  10651  modqmulmod  10652  modqmulmodr  10653  modqsubdir  10656  addmodlteq  10661  nninfinf  10706  iseqf1olemab  10765  iseqf1olemmo  10768  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seqf1oglem1  10782  seqf1oglem2  10783  seqf1og  10784  exp3val  10804  expcl2lemap  10814  expap0  10832  expnegzap  10836  expmul  10847  leexp1a  10857  qsqeqor  10913  expnbnd  10926  nn0ltexp2  10972  nn0opth2  10987  facndiv  11002  faclbnd  11004  bcval5  11026  bcpasc  11029  hashennnuni  11042  hashunlem  11068  hashunsng  11072  hashprg  11073  fiprsshashgt1  11082  hashxp  11091  fimaxq  11092  zfz1isolemiso  11104  zfz1isolem1  11105  seq3coll  11107  iswrdiz  11121  wrdnval  11145  ccatlen  11173  ccatvalfn  11179  ccatsymb  11180  ccatalpha  11191  ccat2s1fstg  11226  swrdclg  11232  swrdsb0eq  11247  pfxwrdsymbg  11272  wrdind  11304  wrd2ind  11305  swrdccatin2  11311  pfxccatin12lem2  11313  pfxccatin12  11315  pfxccat3  11316  swrdccat  11317  shftlem  11378  shftfvalg  11380  shftfval  11383  2shfti  11393  caucvgrelemrec  11541  caucvgrelemcau  11542  caucvgre  11543  cvg1nlemcau  11546  cvg1nlemres  11547  resqrexlemcalc3  11578  resqrexlemcvg  11581  resqrexlemglsq  11584  resqrexlemga  11585  sqrtsq  11606  leabs  11636  absexpzap  11642  abslt  11650  absle  11651  abssubap0  11652  caubnd2  11679  icodiamlt  11742  maxleim  11767  maxabslemval  11770  maxleastlt  11777  rexico  11783  zmaxcl  11786  fimaxre2  11789  minmax  11792  xrmaxleim  11806  xrmaxiflemcl  11807  xrmaxifle  11808  xrmaxiflemlub  11810  xrmaxiflemval  11812  xrmaxleastlt  11818  xrmaxltsup  11820  xrmaxadd  11823  xrminmax  11827  xrbdtri  11838  climuni  11855  climshftlemg  11864  iserex  11901  climcau  11909  climrecvg1n  11910  climcvg1nlem  11911  sumeq2  11921  summodclem3  11943  zsumdc  11947  isumss  11954  fisumss  11955  sumsnf  11972  fsumconst  12017  modfsummod  12021  fsum00  12025  fsumabs  12028  fsumrelem  12034  fsumiun  12040  isumsplit  12054  divcnv  12060  geo2sum  12077  geoisumr  12081  cvgratz  12095  ntrivcvgap  12111  prodeq2  12120  prodmodclem2  12140  prodmodc  12141  zproddc  12142  fprodmul  12154  prodsnf  12155  fprodcl2lem  12168  fprodconst  12183  fprodap0  12184  fprodrec  12192  fprodap0f  12199  fprodle  12203  fprodmodd  12204  tanaddap  12302  zdvdsdc  12375  dvds2ln  12387  fsumdvds  12405  dvdsle  12407  dvdsext  12418  divalglemeunn  12484  divalglemex  12485  divalglemeuneg  12486  bitsfzo  12518  bitsmod  12519  bitsinv1lem  12524  bitsinv1  12525  dvdsbnd  12529  gcdsupex  12530  gcdsupcl  12531  dvdslegcd  12537  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemmain  12571  bezoutlemzz  12575  bezoutlembz  12577  bezoutlembi  12578  bezoutlemle  12581  dfgcd3  12583  bezout  12584  dfgcd2  12587  dvdsmulgcd  12598  bezoutr  12605  uzwodc  12610  nninfctlemfo  12613  lcmval  12637  lcmcllem  12641  lcmneg  12648  ncoprmgcdne1b  12663  isprm2lem  12690  prmind2  12694  dvdsnprmd  12699  isprm5  12716  prmdvdsexp  12722  sqrt2irr  12736  oddpwdclemxy  12743  oddpwdclemdc  12747  nonsq  12781  pceu  12870  pcmul  12876  pc2dvds  12905  pcz  12907  pcprmpw2  12908  dvdsprmpweqle  12912  pcfac  12925  qexpz  12927  prmpwdvds  12930  1arith  12942  mul4sq  12969  4sqexercise2  12974  4sqlemsdc  12975  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemhom  13038  ennnfonelemfun  13040  ennnfonelemf1  13041  ennnfonelemim  13047  exmidunben  13049  ctiunctlemfo  13062  omiunct  13067  ssnnctlemct  13069  isstruct2r  13095  prdsval  13358  ismgm  13442  issgrp  13488  sgrppropd  13498  sgrpidmndm  13505  mndpropd  13525  issubmnd  13527  prdsidlem  13532  resmhm2b  13574  gsumwmhm  13583  isgrpinv  13639  grplmulf1o  13659  dfgrp3mlem  13683  grplactcnv  13687  pwssub  13698  mhmid  13704  mhmmnd  13705  ghmgrp  13707  mulgval  13711  mulgfng  13713  mulgnnp1  13719  mulgnn0dir  13741  mulgneg2  13745  mhmmulg  13752  grpissubg  13783  isnsg  13791  isnsg3  13796  nmzsubg  13799  ghmmhmb  13843  ghmpreima  13855  ghmnsgpreima  13858  ghmf1  13862  ghmf1o  13864  conjghm  13865  conjnmz  13868  conjnmzb  13869  ghmcmn  13916  gsumfzconst  13930  issrg  13981  srglmhm  14009  srgrmhm  14010  isring  14016  ringadd2  14043  ringlghm  14077  ringrghm  14078  oppr1g  14098  dvdsrvald  14110  dvdsrd  14111  dvdsrex  14115  dvdsrmul1  14119  unitgrp  14133  rhmopp  14193  subrgintm  14260  subrgpropd  14270  isdomn  14286  lmodprop2d  14365  lssvacl  14382  lssvsubcl  14383  lssvscl  14392  lsslss  14398  lss1d  14400  lsspropdg  14448  expghmap  14624  mulgghm2  14625  znunit  14676  znrrg  14677  mplvalcoe  14707  mplsubgfilemcl  14716  mplsubgfileminv  14717  mplsubgfi  14718  opnssneib  14883  restbasg  14895  restopn2  14910  iscnp4  14945  cnss2  14954  cnconst2  14960  cnptopresti  14965  cnptoprest2  14967  neitx  14995  uptx  15001  txrest  15003  txdis1cn  15005  xmetres2  15106  xblss2ps  15131  blhalf  15135  blssps  15154  blss  15155  blssexps  15156  blssex  15157  blin2  15159  metequiv2  15223  bdmetval  15227  metcnp3  15238  metcnp  15239  metcn  15241  metcnpi  15242  metcnpi2  15243  txmetcnp  15245  txmetcn  15246  qtopbas  15249  tgqioo  15282  mpomulcn  15293  fsumcncntop  15294  elcncf2  15301  mulcncflem  15334  mulcncf  15335  suplociccreex  15351  limcdifap  15389  cnplimcim  15394  cnplimccntop  15397  limccnpcntop  15402  dvcj  15436  dvmptfsum  15452  dveflem  15453  ply1termlem  15469  plyaddlem1  15474  plymullem1  15475  plycolemc  15485  plycjlemc  15487  plyrecj  15490  dvply1  15492  reeff1olem  15498  eflt  15502  sin0pilem1  15508  ptolemy  15551  coseq0q4123  15561  coseq0negpitopi  15563  cos02pilt1  15578  cos11  15580  ioocosf1o  15581  rpcxpmul2  15640  cxplt  15643  cxple  15644  cxplt3  15647  apcxp2  15666  rprelogbmul  15682  rprelogbdiv  15684  dvdsppwf1o  15716  perfect  15728  lgsval  15736  lgsfcl2  15738  lgscllem  15739  lgsval2lem  15742  lgsdir2lem4  15763  lgsdir2lem5  15764  lgsdir2  15765  lgsne0  15770  gausslemma2dlem1a  15790  gausslemma2dlem1f1o  15792  2sqlem6  15852  2sqlem10  15857  umgrnloopv  15968  umgrvad2edg  16065  usgr1eop  16099  wlkvtxiedg  16199  wlkvtxiedgg  16200  upgredginwlk  16210  upgriswlkdc  16214  clwwlkccatlem  16254  eupth2lem3lem4fi  16327  pw1ndom3  16610  2omap  16615  pw1map  16617  pwle2  16620  pwf1oexmid  16621  subctctexmid  16622  pw1nct  16625  peano4nninf  16629  nninfalllem1  16631  nninfall  16632  nninfsellemeq  16637  nninfsellemqall  16638  nnnninfex  16645  nninfnfiinf  16646  sbthom  16651  refeq  16653  isomninnlem  16655  trilpolemeq1  16665  trilpolemlt1  16666  trirec0  16669  apdiff  16673  iswomninnlem  16674  ismkvnnlem  16677  redcwlpolemeq1  16679  ltlenmkv  16695  gfsumcl  16708