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  1085  simp2lr  1089  simp3lr  1093  bilukdc  1438  dcun  3601  ifnefals  3647  intab  3952  exmid01  4282  exmidundif  4290  exmidundifim  4291  frirrg  4441  reg2exmidlema  4626  imadiflem  5400  fvco4  5708  fvmptt  5728  fcoconst  5808  funopsn  5819  f1imass  5904  fcof1  5913  fliftfun  5926  riotass2  5989  ovmpodxf  6136  dftpos4  6415  tfrlem1  6460  tfrlem3ag  6461  tfrlemibacc  6478  tfrlemibfn  6480  tfrlemi1  6484  tfrlemi14d  6485  tfr1onlem3ag  6489  tfr1onlembacc  6494  tfr1onlembfn  6496  tfr1onlemaccex  6500  tfrcllembacc  6507  tfrcllembfn  6509  tfrcllemaccex  6513  frecabcl  6551  nntr2  6657  dcdifsnid  6658  nnm00  6684  ecopovsymg  6789  ecopoverg  6791  th3qlem1  6792  mapss  6846  f1imaen2g  6953  pw2f1odclem  7003  xpen  7014  xpmapenlem  7018  phpm  7035  fidifsnen  7040  dif1enen  7050  fiunsnnn  7051  fin0  7055  fin0or  7056  findcard2d  7061  findcard2sd  7062  diffifi  7064  isinfinf  7067  tridc  7069  fimax2gtrilemstep  7070  fimax2gtri  7071  en2eqpr  7077  onunsnss  7087  unsnfidcex  7090  unsnfidcel  7091  undifdcss  7093  unfiin  7096  fisseneq  7104  ssfirab  7106  f1finf1o  7122  fidcenumlemrks  7128  fidcenumlemrk  7129  fidcenumlemr  7130  fidcenum  7131  suplub2ti  7176  supisolem  7183  ordiso2  7210  djudom  7268  omp1eomlem  7269  difinfsnlem  7274  difinfinf  7276  ctm  7284  ctssdclemn0  7285  enumct  7290  nnnninfeq  7303  nnnninfeq2  7304  nninfisol  7308  enomnilem  7313  finomni  7315  exmidomni  7317  fodju0  7322  ismkvnex  7330  enmkvlem  7336  enwomnilem  7344  pr2cv1  7376  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  exmidaclem  7398  exmidontriimlem1  7411  exmidontriimlem2  7412  exmidontriimlem3  7413  exmidontriimlem4  7414  exmidontriim  7415  netap  7448  exmidapne  7454  dfplpq2  7549  dfmpq2  7550  mulpipqqs  7568  nqpi  7573  distrnqg  7582  prarloclemarch  7613  enq0tr  7629  nqnq0pi  7633  nq0nn  7637  nnnq0lem1  7641  prarloclemup  7690  prarloclem3  7692  prarloclemcalc  7697  genplt2i  7705  addnqprllem  7722  addnqprulem  7723  appdivnq  7758  distrlem1prl  7777  distrlem1pru  7778  ltaddpr  7792  ltexprlemlol  7797  ltexprlemupu  7799  ltexprlemdisj  7801  addcanprleml  7809  ltaprlem  7813  addextpr  7816  recexprlemopu  7822  recexprlemdisj  7825  recexprlem1ssl  7828  aptiprleml  7834  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemlol  7842  cauappcvgprlemopu  7843  cauappcvgprlemdisj  7846  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemopu  7866  caucvgprlemladdfu  7872  caucvgprprlemml  7889  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemopu  7894  caucvgprprlemexbt  7901  suplocexprlemru  7914  suplocexprlemloc  7916  suplocexprlemub  7918  suplocexprlemlub  7919  prsrlem1  7937  recexgt0sr  7968  mulgt0sr  7973  archsr  7977  caucvgsrlemcau  7988  caucvgsrlemoffcau  7993  caucvgsrlemoffres  7995  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  addcnsr  8029  mulcnsr  8030  mulcnsrec  8038  axmulcom  8066  nntopi  8089  axcaucvglemcau  8093  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  mpomulf  8144  axsuploc  8227  ltntri  8282  cnegexlem2  8330  cnegexlem3  8331  addsub4  8397  le2add  8599  lt2add  8600  lt2sub  8615  le2sub  8616  rereim  8741  apreim  8758  mulreim  8759  apcotr  8762  apadd1  8763  addext  8765  mulext1  8767  mulext  8769  apti  8777  aptap  8805  receuap  8824  rec11rap  8866  divdivdivap  8868  divadddivap  8882  divsubdivap  8883  rerecclap  8885  recgt0  9005  prodgt0gt0  9006  prodgt0  9007  prodge0  9009  lemulge11  9021  lt2mul2div  9034  ltrec  9038  lerec  9039  ltrec1  9043  lediv2a  9050  mulle0r  9099  sup3exmid  9112  zdiv  9543  eluzuzle  9738  supinfneg  9798  infsupneg  9799  infregelbex  9801  xrltso  10000  xnn0dcle  10006  xnn0letri  10007  npnflt  10019  nmnfgt  10022  z2ge  10030  xaddf  10048  xaddval  10049  xpncan  10075  xleadd1a  10077  xltadd1  10080  xaddge0  10082  xle2add  10083  xleaddadd  10091  ixxss1  10108  ixxss2  10109  elico2  10141  iccsupr  10170  fzass4  10266  fzrev  10288  fz0fzelfz0  10331  fzocatel  10413  elfzomelpfzo  10445  zsupcllemstep  10457  exbtwnzlemstep  10475  rebtwn2zlemstep  10480  qbtwnxr  10485  xqltnle  10495  apbtwnz  10502  btwnzge0  10528  modqid  10579  modqcyc  10589  modqcyc2  10590  modqaddabs  10592  modqaddmod  10593  mulqaddmodid  10594  modqmuladd  10596  modqltm1p1mod  10606  modqsubmod  10612  modqsubmodmod  10613  modaddmodlo  10618  modqmulmod  10619  modqmulmodr  10620  modqsubdir  10623  addmodlteq  10628  nninfinf  10673  iseqf1olemab  10732  iseqf1olemmo  10735  iseqf1olemjpcl  10738  iseqf1olemqpcl  10739  seqf1oglem1  10749  seqf1oglem2  10750  seqf1og  10751  exp3val  10771  expcl2lemap  10781  expap0  10799  expnegzap  10803  expmul  10814  leexp1a  10824  qsqeqor  10880  expnbnd  10893  nn0ltexp2  10939  nn0opth2  10954  facndiv  10969  faclbnd  10971  bcval5  10993  bcpasc  10996  hashennnuni  11009  hashunlem  11034  hashunsng  11037  hashprg  11038  fiprsshashgt1  11047  hashxp  11056  fimaxq  11057  zfz1isolemiso  11069  zfz1isolem1  11070  seq3coll  11072  iswrdiz  11086  wrdnval  11110  ccatlen  11138  ccatvalfn  11144  ccatsymb  11145  swrdclg  11190  swrdsb0eq  11205  pfxwrdsymbg  11230  wrdind  11262  wrd2ind  11263  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12  11273  pfxccat3  11274  swrdccat  11275  shftlem  11335  shftfvalg  11337  shftfval  11340  2shfti  11350  caucvgrelemrec  11498  caucvgrelemcau  11499  caucvgre  11500  cvg1nlemcau  11503  cvg1nlemres  11504  resqrexlemcalc3  11535  resqrexlemcvg  11538  resqrexlemglsq  11541  resqrexlemga  11542  sqrtsq  11563  leabs  11593  absexpzap  11599  abslt  11607  absle  11608  abssubap0  11609  caubnd2  11636  icodiamlt  11699  maxleim  11724  maxabslemval  11727  maxleastlt  11734  rexico  11740  zmaxcl  11743  fimaxre2  11746  minmax  11749  xrmaxleim  11763  xrmaxiflemcl  11764  xrmaxifle  11765  xrmaxiflemlub  11767  xrmaxiflemval  11769  xrmaxleastlt  11775  xrmaxltsup  11777  xrmaxadd  11780  xrminmax  11784  xrbdtri  11795  climuni  11812  climshftlemg  11821  iserex  11858  climcau  11866  climrecvg1n  11867  climcvg1nlem  11868  sumeq2  11878  summodclem3  11899  zsumdc  11903  isumss  11910  fisumss  11911  sumsnf  11928  fsumconst  11973  modfsummod  11977  fsum00  11981  fsumabs  11984  fsumrelem  11990  fsumiun  11996  isumsplit  12010  divcnv  12016  geo2sum  12033  geoisumr  12037  cvgratz  12051  ntrivcvgap  12067  prodeq2  12076  prodmodclem2  12096  prodmodc  12097  zproddc  12098  fprodmul  12110  prodsnf  12111  fprodcl2lem  12124  fprodconst  12139  fprodap0  12140  fprodrec  12148  fprodap0f  12155  fprodle  12159  fprodmodd  12160  tanaddap  12258  zdvdsdc  12331  dvds2ln  12343  fsumdvds  12361  dvdsle  12363  dvdsext  12374  divalglemeunn  12440  divalglemex  12441  divalglemeuneg  12442  bitsfzo  12474  bitsmod  12475  bitsinv1lem  12480  bitsinv1  12481  dvdsbnd  12485  gcdsupex  12486  gcdsupcl  12487  dvdslegcd  12493  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlemzz  12531  bezoutlembz  12533  bezoutlembi  12534  bezoutlemle  12537  dfgcd3  12539  bezout  12540  dfgcd2  12543  dvdsmulgcd  12554  bezoutr  12561  uzwodc  12566  nninfctlemfo  12569  lcmval  12593  lcmcllem  12597  lcmneg  12604  ncoprmgcdne1b  12619  isprm2lem  12646  prmind2  12650  dvdsnprmd  12655  isprm5  12672  prmdvdsexp  12678  sqrt2irr  12692  oddpwdclemxy  12699  oddpwdclemdc  12703  nonsq  12737  pceu  12826  pcmul  12832  pc2dvds  12861  pcz  12863  pcprmpw2  12864  dvdsprmpweqle  12868  pcfac  12881  qexpz  12883  prmpwdvds  12886  1arith  12898  mul4sq  12925  4sqexercise2  12930  4sqlemsdc  12931  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemhom  12994  ennnfonelemfun  12996  ennnfonelemf1  12997  ennnfonelemim  13003  exmidunben  13005  ctiunctlemfo  13018  omiunct  13023  ssnnctlemct  13025  isstruct2r  13051  prdsval  13314  ismgm  13398  issgrp  13444  sgrppropd  13454  sgrpidmndm  13461  mndpropd  13481  issubmnd  13483  prdsidlem  13488  resmhm2b  13530  gsumwmhm  13539  isgrpinv  13595  grplmulf1o  13615  dfgrp3mlem  13639  grplactcnv  13643  pwssub  13654  mhmid  13660  mhmmnd  13661  ghmgrp  13663  mulgval  13667  mulgfng  13669  mulgnnp1  13675  mulgnn0dir  13697  mulgneg2  13701  mhmmulg  13708  grpissubg  13739  isnsg  13747  isnsg3  13752  nmzsubg  13755  ghmmhmb  13799  ghmpreima  13811  ghmnsgpreima  13814  ghmf1  13818  ghmf1o  13820  conjghm  13821  conjnmz  13824  conjnmzb  13825  ghmcmn  13872  gsumfzconst  13886  issrg  13936  srglmhm  13964  srgrmhm  13965  isring  13971  ringadd2  13998  ringlghm  14032  ringrghm  14033  oppr1g  14053  dvdsrvald  14065  dvdsrd  14066  dvdsrex  14070  dvdsrmul1  14074  unitgrp  14088  rhmopp  14148  subrgintm  14215  subrgpropd  14225  isdomn  14241  lmodprop2d  14320  lssvacl  14337  lssvsubcl  14338  lssvscl  14347  lsslss  14353  lss1d  14355  lsspropdg  14403  expghmap  14579  mulgghm2  14580  znunit  14631  znrrg  14632  mplvalcoe  14662  mplsubgfilemcl  14671  mplsubgfileminv  14672  mplsubgfi  14673  opnssneib  14838  restbasg  14850  restopn2  14865  iscnp4  14900  cnss2  14909  cnconst2  14915  cnptopresti  14920  cnptoprest2  14922  neitx  14950  uptx  14956  txrest  14958  txdis1cn  14960  xmetres2  15061  xblss2ps  15086  blhalf  15090  blssps  15109  blss  15110  blssexps  15111  blssex  15112  blin2  15114  metequiv2  15178  bdmetval  15182  metcnp3  15193  metcnp  15194  metcn  15196  metcnpi  15197  metcnpi2  15198  txmetcnp  15200  txmetcn  15201  qtopbas  15204  tgqioo  15237  mpomulcn  15248  fsumcncntop  15249  elcncf2  15256  mulcncflem  15289  mulcncf  15290  suplociccreex  15306  limcdifap  15344  cnplimcim  15349  cnplimccntop  15352  limccnpcntop  15357  dvcj  15391  dvmptfsum  15407  dveflem  15408  ply1termlem  15424  plyaddlem1  15429  plymullem1  15430  plycolemc  15440  plycjlemc  15442  plyrecj  15445  dvply1  15447  reeff1olem  15453  eflt  15457  sin0pilem1  15463  ptolemy  15506  coseq0q4123  15516  coseq0negpitopi  15518  cos02pilt1  15533  cos11  15535  ioocosf1o  15536  rpcxpmul2  15595  cxplt  15598  cxple  15599  cxplt3  15602  apcxp2  15621  rprelogbmul  15637  rprelogbdiv  15639  dvdsppwf1o  15671  perfect  15683  lgsval  15691  lgsfcl2  15693  lgscllem  15694  lgsval2lem  15697  lgsdir2lem4  15718  lgsdir2lem5  15719  lgsdir2  15720  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  2sqlem6  15807  2sqlem10  15812  umgrnloopv  15922  umgrvad2edg  16017  wlkvtxiedg  16066  wlkvtxiedgg  16067  upgredginwlk  16077  upgriswlkdc  16081  pw1ndom3  16383  2omap  16388  pw1map  16390  pwle2  16393  pwf1oexmid  16394  subctctexmid  16395  pw1nct  16398  peano4nninf  16402  nninfalllem1  16404  nninfall  16405  nninfsellemeq  16410  nninfsellemqall  16411  nnnninfex  16418  nninfnfiinf  16419  sbthom  16424  refeq  16426  isomninnlem  16428  trilpolemeq1  16438  trilpolemlt1  16439  trirec0  16442  apdiff  16446  iswomninnlem  16447  ismkvnnlem  16450  redcwlpolemeq1  16452  ltlenmkv  16468