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  3621  ifnefals  3669  intab  3980  exmid01  4313  exmidundif  4321  exmidundifim  4322  frirrg  4473  reg2exmidlema  4658  imadiflem  5437  fvco4  5751  fvmptt  5771  fcoconst  5850  funopsn  5862  f1imass  5949  fcof1  5958  fliftfun  5971  riotass2  6034  ovmpodxf  6181  fsuppeq  6449  fsuppeqg  6450  suppssdc  6462  suppssfvg  6465  dftpos4  6496  tfrlem1  6541  tfrlem3ag  6542  tfrlemibacc  6559  tfrlemibfn  6561  tfrlemi1  6565  tfrlemi14d  6566  tfr1onlem3ag  6570  tfr1onlembacc  6575  tfr1onlembfn  6577  tfr1onlemaccex  6581  tfrcllembacc  6588  tfrcllembfn  6590  tfrcllemaccex  6594  frecabcl  6632  nntr2  6738  dcdifsnid  6739  nnm00  6765  ecopovsymg  6870  ecopoverg  6872  th3qlem1  6873  mapss  6928  f1imaen2g  7035  pw2f1odclem  7089  xpen  7100  xpmapenlem  7104  mapunen  7106  phpm  7122  fidifsnen  7127  dif1enen  7139  fiunsnnn  7140  fin0  7144  fin0or  7145  findcard2d  7150  findcard2sd  7151  diffifi  7153  isinfinf  7156  tridc  7159  fimax2gtrilemstep  7160  fimax2gtri  7161  en2eqpr  7169  onunsnss  7179  unsnfidcex  7182  unsnfidcel  7183  undifdcss  7185  unfiin  7188  fisseneq  7197  ssfirab  7199  f1finf1o  7219  fidcenumlemrks  7225  fidcenumlemrk  7226  fidcenumlemr  7227  fidcenum  7228  ffsuppbi  7255  2omap  7271  suplub2ti  7294  supisolem  7301  ordiso2  7328  djudom  7386  omp1eomlem  7387  difinfsnlem  7392  difinfinf  7394  ctm  7402  ctssdclemn0  7403  enumct  7408  nnnninfeq  7421  nnnninfeq2  7422  nninfisol  7426  enomnilem  7431  finomni  7433  exmidomni  7435  fodju0  7440  ismkvnex  7448  enmkvlem  7454  enwomnilem  7462  pr2cv1  7494  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidaclem  7517  exmidontriimlem1  7530  exmidontriimlem2  7531  exmidontriimlem3  7532  exmidontriimlem4  7533  exmidontriim  7534  netap  7573  exmidapne  7579  dfplpq2  7674  dfmpq2  7675  mulpipqqs  7693  nqpi  7698  distrnqg  7707  prarloclemarch  7738  enq0tr  7754  nqnq0pi  7758  nq0nn  7762  nnnq0lem1  7766  prarloclemup  7815  prarloclem3  7817  prarloclemcalc  7822  genplt2i  7830  addnqprllem  7847  addnqprulem  7848  appdivnq  7883  distrlem1prl  7902  distrlem1pru  7903  ltaddpr  7917  ltexprlemlol  7922  ltexprlemupu  7924  ltexprlemdisj  7926  addcanprleml  7934  ltaprlem  7938  addextpr  7941  recexprlemopu  7947  recexprlemdisj  7950  recexprlem1ssl  7953  aptiprleml  7959  cauappcvgprlemm  7965  cauappcvgprlemopl  7966  cauappcvgprlemlol  7967  cauappcvgprlemopu  7968  cauappcvgprlemdisj  7971  cauappcvgprlemladdfu  7974  cauappcvgprlemladdfl  7975  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  caucvgprlemm  7988  caucvgprlemopl  7989  caucvgprlemlol  7990  caucvgprlemopu  7991  caucvgprlemladdfu  7997  caucvgprprlemml  8014  caucvgprprlemopl  8017  caucvgprprlemlol  8018  caucvgprprlemopu  8019  caucvgprprlemexbt  8026  suplocexprlemru  8039  suplocexprlemloc  8041  suplocexprlemub  8043  suplocexprlemlub  8044  prsrlem1  8062  recexgt0sr  8093  mulgt0sr  8098  archsr  8102  caucvgsrlemcau  8113  caucvgsrlemoffcau  8118  caucvgsrlemoffres  8120  suplocsrlemb  8126  suplocsrlempr  8127  suplocsrlem  8128  addcnsr  8154  mulcnsr  8155  mulcnsrec  8163  axmulcom  8191  nntopi  8214  axcaucvglemcau  8218  axcaucvglemres  8219  axpre-suploclemres  8221  axpre-suploc  8222  mpomulf  8269  axsuploc  8351  ltntri  8406  cnegexlem2  8454  cnegexlem3  8455  addsub4  8521  le2add  8723  lt2add  8724  lt2sub  8739  le2sub  8740  rereim  8865  apreim  8882  mulreim  8883  apcotr  8886  apadd1  8887  addext  8889  mulext1  8891  mulext  8893  apti  8901  aptap  8929  receuap  8948  rec11rap  8990  divdivdivap  8992  divadddivap  9006  divsubdivap  9007  rerecclap  9009  recgt0  9129  prodgt0gt0  9130  prodgt0  9131  prodge0  9133  lemulge11  9145  lt2mul2div  9158  ltrec  9162  lerec  9163  ltrec1  9167  lediv2a  9174  mulle0r  9223  sup3exmid  9236  zdiv  9672  eluzuzle  9868  supinfneg  9933  infsupneg  9934  infregelbex  9936  xrltso  10135  xnn0dcle  10141  xnn0letri  10142  npnflt  10154  nmnfgt  10157  z2ge  10165  xaddf  10183  xaddval  10184  xpncan  10210  xleadd1a  10212  xltadd1  10215  xaddge0  10217  xle2add  10218  xleaddadd  10226  ixxss1  10243  ixxss2  10244  elico2  10276  iccsupr  10305  fzass4  10402  fzrev  10425  fz0fzelfz0  10468  fzocatel  10551  elfzomelpfzo  10583  zsupcllemstep  10596  exbtwnzlemstep  10614  rebtwn2zlemstep  10619  qbtwnxr  10624  xqltnle  10634  apbtwnz  10641  btwnzge0  10667  modqid  10718  modqcyc  10728  modqcyc2  10729  modqaddabs  10731  modqaddmod  10732  mulqaddmodid  10733  modqmuladd  10735  modqltm1p1mod  10745  modqsubmod  10751  modqsubmodmod  10752  modaddmodlo  10757  modqmulmod  10758  modqmulmodr  10759  modqsubdir  10762  addmodlteq  10767  nninfinf  10812  iseqf1olemab  10871  iseqf1olemmo  10874  iseqf1olemjpcl  10877  iseqf1olemqpcl  10878  seqf1oglem1  10888  seqf1oglem2  10889  seqf1og  10890  exp3val  10910  expcl2lemap  10920  expap0  10938  expnegzap  10942  expmul  10953  leexp1a  10963  qsqeqor  11019  resq01  11027  expnbnd  11033  nn0ltexp2  11079  nn0opth2  11094  facndiv  11109  faclbnd  11111  bcval5  11133  bcpasc  11136  hashennnuni  11150  hashunlem  11176  hashunsng  11180  hashprg  11181  fiprsshashgt1  11190  hashxp  11199  fimaxq  11202  hashfibc  11215  zfz1isolemiso  11219  zfz1isolem1  11220  seq3coll  11222  iswrdiz  11239  wrdnval  11263  ccatlen  11291  ccatvalfn  11297  ccatsymb  11298  ccatalpha  11309  ccat2s1fstg  11344  swrdclg  11350  swrdsb0eq  11365  pfxwrdsymbg  11390  wrdind  11422  wrd2ind  11423  swrdccatin2  11429  pfxccatin12lem2  11431  pfxccatin12  11433  pfxccat3  11434  swrdccat  11435  shftlem  11509  shftfvalg  11511  shftfval  11514  2shfti  11524  caucvgrelemrec  11672  caucvgrelemcau  11673  caucvgre  11674  cvg1nlemcau  11677  cvg1nlemres  11678  resqrexlemcalc3  11709  resqrexlemcvg  11712  resqrexlemglsq  11715  resqrexlemga  11716  sqrtsq  11737  leabs  11767  absexpzap  11773  abslt  11781  absle  11782  abssubap0  11783  caubnd2  11810  icodiamlt  11873  maxleim  11898  maxabslemval  11901  maxleastlt  11908  rexico  11914  zmaxcl  11917  fimaxre2  11920  minmax  11923  xrmaxleim  11937  xrmaxiflemcl  11938  xrmaxifle  11939  xrmaxiflemlub  11941  xrmaxiflemval  11943  xrmaxleastlt  11949  xrmaxltsup  11951  xrmaxadd  11954  xrminmax  11958  xrbdtri  11969  climuni  11986  climshftlemg  11995  iserex  12032  climcau  12040  climrecvg1n  12041  climcvg1nlem  12042  sumeq2  12052  summodclem3  12074  zsumdc  12078  isumss  12085  fisumss  12086  sumsnf  12103  fsumconst  12148  modfsummod  12152  fsum00  12156  fsumabs  12159  fsumrelem  12165  fsumiun  12171  isumsplit  12185  divcnv  12191  geo2sum  12208  geoisumr  12212  cvgratz  12226  ntrivcvgap  12242  prodeq2  12251  prodmodclem2  12271  prodmodc  12272  zproddc  12273  fprodmul  12285  prodsnf  12286  fprodcl2lem  12299  fprodconst  12314  fprodap0  12315  fprodrec  12323  fprodap0f  12330  fprodle  12334  fprodmodd  12335  tanaddap  12433  zdvdsdc  12506  dvds2ln  12518  fsumdvds  12536  dvdsle  12538  dvdsext  12549  divalglemeunn  12615  divalglemex  12616  divalglemeuneg  12617  bitsfzo  12649  bitsmod  12650  bitsinv1lem  12655  bitsinv1  12656  dvdsbnd  12660  gcdsupex  12661  gcdsupcl  12662  dvdslegcd  12668  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemmain  12702  bezoutlemzz  12706  bezoutlembz  12708  bezoutlembi  12709  bezoutlemle  12712  dfgcd3  12714  bezout  12715  dfgcd2  12718  dvdsmulgcd  12729  bezoutr  12736  uzwodc  12741  nninfctlemfo  12744  lcmval  12768  lcmcllem  12772  lcmneg  12779  ncoprmgcdne1b  12794  isprm2lem  12821  prmind2  12825  dvdsnprmd  12830  isprm5  12847  prmdvdsexp  12853  sqrt2irr  12867  oddpwdclemxy  12874  oddpwdclemdc  12878  nonsq  12912  pceu  13001  pcmul  13007  pc2dvds  13036  pcz  13038  pcprmpw2  13039  dvdsprmpweqle  13043  pcfac  13056  qexpz  13058  prmpwdvds  13061  1arith  13073  mul4sq  13100  4sqexercise2  13105  4sqlemsdc  13106  ballotfilem2  13153  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemhom  13187  ennnfonelemfun  13189  ennnfonelemf1  13190  ennnfonelemim  13196  exmidunben  13198  ctiunctlemfo  13211  omiunct  13216  ssnnctlemct  13218  isstruct2r  13244  prdsval  13507  ismgm  13591  issgrp  13637  sgrppropd  13647  sgrpidmndm  13654  mndpropd  13674  issubmnd  13676  prdsidlem  13681  resmhm2b  13723  gsumwmhm  13732  isgrpinv  13788  grplmulf1o  13808  dfgrp3mlem  13832  grplactcnv  13836  pwssub  13847  mhmid  13853  mhmmnd  13854  ghmgrp  13856  mulgval  13860  mulgfng  13862  mulgnnp1  13868  mulgnn0dir  13890  mulgneg2  13894  mhmmulg  13901  grpissubg  13932  isnsg  13940  isnsg3  13945  nmzsubg  13948  ghmmhmb  13992  ghmpreima  14004  ghmnsgpreima  14007  ghmf1  14011  ghmf1o  14013  conjghm  14014  conjnmz  14017  conjnmzb  14018  ghmcmn  14065  gsumfzconst  14079  issrg  14130  srglmhm  14158  srgrmhm  14159  isring  14165  ringadd2  14192  ringlghm  14226  ringrghm  14227  oppr1g  14248  dvdsrvald  14260  dvdsrd  14261  dvdsrex  14265  dvdsrmul1  14269  unitgrp  14283  rhmopp  14343  subrgintm  14411  subrgpropd  14421  isdomn  14438  aprnzr  14459  opprdrng  14480  lmodprop2d  14545  lssvacl  14562  lssvsubcl  14563  lssvscl  14572  lsslss  14578  lss1d  14580  lsspropdg  14628  expghmap  14804  mulgghm2  14805  znunit  14856  znrrg  14857  mplvalcoe  14894  mplsubgfilemcl  14903  mplsubgfileminv  14904  mplsubgfi  14905  opnssneib  15070  restbasg  15082  restopn2  15097  iscnp4  15132  cnss2  15141  cnconst2  15147  cnptopresti  15152  cnptoprest2  15154  neitx  15182  uptx  15188  txrest  15190  txdis1cn  15192  xmetres2  15293  xblss2ps  15318  blhalf  15322  blssps  15341  blss  15342  blssexps  15343  blssex  15344  blin2  15346  metequiv2  15410  bdmetval  15414  metcnp3  15425  metcnp  15426  metcn  15428  metcnpi  15429  metcnpi2  15430  txmetcnp  15432  txmetcn  15433  qtopbas  15436  tgqioo  15469  mpomulcn  15480  fsumcncntop  15481  elcncf2  15488  mulcncflem  15521  mulcncf  15522  suplociccreex  15538  limcdifap  15576  cnplimcim  15581  cnplimccntop  15584  limccnpcntop  15589  dvcj  15623  dvmptfsum  15639  dveflem  15640  ply1termlem  15656  plyaddlem1  15661  plymullem1  15662  plycolemc  15672  plycjlemc  15674  plyrecj  15677  dvply1  15679  reeff1olem  15685  eflt  15689  sin0pilem1  15695  ptolemy  15738  coseq0q4123  15748  coseq0negpitopi  15750  cos02pilt1  15765  cos11  15767  ioocosf1o  15768  rpcxpmul2  15827  cxplt  15830  cxple  15831  cxplt3  15834  apcxp2  15853  rprelogbmul  15869  rprelogbdiv  15871  pellexlem3  15896  dvdsppwf1o  15906  perfect  15918  lgsval  15926  lgsfcl2  15928  lgscllem  15929  lgsval2lem  15932  lgsdir2lem4  15953  lgsdir2lem5  15954  lgsdir2  15955  lgsne0  15960  gausslemma2dlem1a  15980  gausslemma2dlem1f1o  15982  2sqlem6  16042  2sqlem10  16047  umgrnloopv  16158  umgrvad2edg  16255  usgr1eop  16289  wlkvtxiedg  16389  wlkvtxiedgg  16390  upgredginwlk  16400  upgriswlkdc  16404  clwwlkccatlem  16444  eupth2lem3lem4fi  16517  pw1ndom3  16813  pw1map  16818  pwle2  16821  pwf1oexmid  16822  subctctexmid  16823  pw1nct  16826  peano4nninf  16833  nninfalllem1  16835  nninfall  16836  nninfsellemeq  16841  nninfsellemqall  16842  nnnninfex  16849  nninfnfiinf  16850  sbthom  16855  refeq  16857  isomninnlem  16863  trilpolemeq1  16873  trilpolemlt1  16874  trirec0  16877  apdiff  16881  iswomninnlem  16883  ismkvnnlem  16886  redcwlpolemeq1  16888  trimul0or  16894  ltlenmkv  16905  gfsumz  16918  gfsumcl  16919