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  1064  simp2lr  1068  simp3lr  1072  bilukdc  1416  dcun  3571  ifnefals  3615  intab  3916  exmid01  4246  exmidundif  4254  exmidundifim  4255  frirrg  4401  reg2exmidlema  4586  imadiflem  5358  fvco4  5658  fvmptt  5678  fcoconst  5758  funopsn  5769  f1imass  5850  fcof1  5859  fliftfun  5872  riotass2  5933  ovmpodxf  6078  dftpos4  6356  tfrlem1  6401  tfrlem3ag  6402  tfrlemibacc  6419  tfrlemibfn  6421  tfrlemi1  6425  tfrlemi14d  6426  tfr1onlem3ag  6430  tfr1onlembacc  6435  tfr1onlembfn  6437  tfr1onlemaccex  6441  tfrcllembacc  6448  tfrcllembfn  6450  tfrcllemaccex  6454  frecabcl  6492  nntr2  6596  dcdifsnid  6597  nnm00  6623  ecopovsymg  6728  ecopoverg  6730  th3qlem1  6731  mapss  6785  f1imaen2g  6892  pw2f1odclem  6938  xpen  6949  xpmapenlem  6953  phpm  6969  fidifsnen  6974  dif1enen  6984  fiunsnnn  6985  fin0  6989  fin0or  6990  findcard2d  6995  findcard2sd  6996  diffifi  6998  isinfinf  7001  tridc  7003  fimax2gtrilemstep  7004  fimax2gtri  7005  en2eqpr  7011  onunsnss  7021  unsnfidcex  7024  unsnfidcel  7025  undifdcss  7027  unfiin  7030  fisseneq  7038  ssfirab  7040  f1finf1o  7056  fidcenumlemrks  7062  fidcenumlemrk  7063  fidcenumlemr  7064  fidcenum  7065  suplub2ti  7110  supisolem  7117  ordiso2  7144  djudom  7202  omp1eomlem  7203  difinfsnlem  7208  difinfinf  7210  ctm  7218  ctssdclemn0  7219  enumct  7224  nnnninfeq  7237  nnnninfeq2  7238  nninfisol  7242  enomnilem  7247  finomni  7249  exmidomni  7251  fodju0  7256  ismkvnex  7264  enmkvlem  7270  enwomnilem  7278  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  exmidaclem  7327  exmidontriimlem1  7340  exmidontriimlem2  7341  exmidontriimlem3  7342  exmidontriimlem4  7343  exmidontriim  7344  netap  7373  exmidapne  7379  dfplpq2  7474  dfmpq2  7475  mulpipqqs  7493  nqpi  7498  distrnqg  7507  prarloclemarch  7538  enq0tr  7554  nqnq0pi  7558  nq0nn  7562  nnnq0lem1  7566  prarloclemup  7615  prarloclem3  7617  prarloclemcalc  7622  genplt2i  7630  addnqprllem  7647  addnqprulem  7648  appdivnq  7683  distrlem1prl  7702  distrlem1pru  7703  ltaddpr  7717  ltexprlemlol  7722  ltexprlemupu  7724  ltexprlemdisj  7726  addcanprleml  7734  ltaprlem  7738  addextpr  7741  recexprlemopu  7747  recexprlemdisj  7750  recexprlem1ssl  7753  aptiprleml  7759  cauappcvgprlemm  7765  cauappcvgprlemopl  7766  cauappcvgprlemlol  7767  cauappcvgprlemopu  7768  cauappcvgprlemdisj  7771  cauappcvgprlemladdfu  7774  cauappcvgprlemladdfl  7775  cauappcvgprlemladdru  7776  cauappcvgprlemladdrl  7777  caucvgprlemm  7788  caucvgprlemopl  7789  caucvgprlemlol  7790  caucvgprlemopu  7791  caucvgprlemladdfu  7797  caucvgprprlemml  7814  caucvgprprlemopl  7817  caucvgprprlemlol  7818  caucvgprprlemopu  7819  caucvgprprlemexbt  7826  suplocexprlemru  7839  suplocexprlemloc  7841  suplocexprlemub  7843  suplocexprlemlub  7844  prsrlem1  7862  recexgt0sr  7893  mulgt0sr  7898  archsr  7902  caucvgsrlemcau  7913  caucvgsrlemoffcau  7918  caucvgsrlemoffres  7920  suplocsrlemb  7926  suplocsrlempr  7927  suplocsrlem  7928  addcnsr  7954  mulcnsr  7955  mulcnsrec  7963  axmulcom  7991  nntopi  8014  axcaucvglemcau  8018  axcaucvglemres  8019  axpre-suploclemres  8021  axpre-suploc  8022  mpomulf  8069  axsuploc  8152  ltntri  8207  cnegexlem2  8255  cnegexlem3  8256  addsub4  8322  le2add  8524  lt2add  8525  lt2sub  8540  le2sub  8541  rereim  8666  apreim  8683  mulreim  8684  apcotr  8687  apadd1  8688  addext  8690  mulext1  8692  mulext  8694  apti  8702  aptap  8730  receuap  8749  rec11rap  8791  divdivdivap  8793  divadddivap  8807  divsubdivap  8808  rerecclap  8810  recgt0  8930  prodgt0gt0  8931  prodgt0  8932  prodge0  8934  lemulge11  8946  lt2mul2div  8959  ltrec  8963  lerec  8964  ltrec1  8968  lediv2a  8975  mulle0r  9024  sup3exmid  9037  zdiv  9468  eluzuzle  9663  supinfneg  9723  infsupneg  9724  infregelbex  9726  xrltso  9925  xnn0dcle  9931  xnn0letri  9932  npnflt  9944  nmnfgt  9947  z2ge  9955  xaddf  9973  xaddval  9974  xpncan  10000  xleadd1a  10002  xltadd1  10005  xaddge0  10007  xle2add  10008  xleaddadd  10016  ixxss1  10033  ixxss2  10034  elico2  10066  iccsupr  10095  fzass4  10191  fzrev  10213  fz0fzelfz0  10256  fzocatel  10335  elfzomelpfzo  10367  zsupcllemstep  10379  exbtwnzlemstep  10397  rebtwn2zlemstep  10402  qbtwnxr  10407  xqltnle  10417  apbtwnz  10424  btwnzge0  10450  modqid  10501  modqcyc  10511  modqcyc2  10512  modqaddabs  10514  modqaddmod  10515  mulqaddmodid  10516  modqmuladd  10518  modqltm1p1mod  10528  modqsubmod  10534  modqsubmodmod  10535  modaddmodlo  10540  modqmulmod  10541  modqmulmodr  10542  modqsubdir  10545  addmodlteq  10550  nninfinf  10595  iseqf1olemab  10654  iseqf1olemmo  10657  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  seqf1oglem1  10671  seqf1oglem2  10672  seqf1og  10673  exp3val  10693  expcl2lemap  10703  expap0  10721  expnegzap  10725  expmul  10736  leexp1a  10746  qsqeqor  10802  expnbnd  10815  nn0ltexp2  10861  nn0opth2  10876  facndiv  10891  faclbnd  10893  bcval5  10915  bcpasc  10918  hashennnuni  10931  hashunlem  10956  hashunsng  10959  hashprg  10960  fiprsshashgt1  10969  hashxp  10978  fimaxq  10979  zfz1isolemiso  10991  zfz1isolem1  10992  seq3coll  10994  iswrdiz  11008  wrdnval  11031  ccatlen  11059  ccatvalfn  11065  ccatsymb  11066  swrdclg  11111  swrdsb0eq  11126  pfxwrdsymbg  11149  shftlem  11171  shftfvalg  11173  shftfval  11176  2shfti  11186  caucvgrelemrec  11334  caucvgrelemcau  11335  caucvgre  11336  cvg1nlemcau  11339  cvg1nlemres  11340  resqrexlemcalc3  11371  resqrexlemcvg  11374  resqrexlemglsq  11377  resqrexlemga  11378  sqrtsq  11399  leabs  11429  absexpzap  11435  abslt  11443  absle  11444  abssubap0  11445  caubnd2  11472  icodiamlt  11535  maxleim  11560  maxabslemval  11563  maxleastlt  11570  rexico  11576  zmaxcl  11579  fimaxre2  11582  minmax  11585  xrmaxleim  11599  xrmaxiflemcl  11600  xrmaxifle  11601  xrmaxiflemlub  11603  xrmaxiflemval  11605  xrmaxleastlt  11611  xrmaxltsup  11613  xrmaxadd  11616  xrminmax  11620  xrbdtri  11631  climuni  11648  climshftlemg  11657  iserex  11694  climcau  11702  climrecvg1n  11703  climcvg1nlem  11704  sumeq2  11714  summodclem3  11735  zsumdc  11739  isumss  11746  fisumss  11747  sumsnf  11764  fsumconst  11809  modfsummod  11813  fsum00  11817  fsumabs  11820  fsumrelem  11826  fsumiun  11832  isumsplit  11846  divcnv  11852  geo2sum  11869  geoisumr  11873  cvgratz  11887  ntrivcvgap  11903  prodeq2  11912  prodmodclem2  11932  prodmodc  11933  zproddc  11934  fprodmul  11946  prodsnf  11947  fprodcl2lem  11960  fprodconst  11975  fprodap0  11976  fprodrec  11984  fprodap0f  11991  fprodle  11995  fprodmodd  11996  tanaddap  12094  zdvdsdc  12167  dvds2ln  12179  fsumdvds  12197  dvdsle  12199  dvdsext  12210  divalglemeunn  12276  divalglemex  12277  divalglemeuneg  12278  bitsfzo  12310  bitsmod  12311  bitsinv1lem  12316  bitsinv1  12317  dvdsbnd  12321  gcdsupex  12322  gcdsupcl  12323  dvdslegcd  12329  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemmain  12363  bezoutlemzz  12367  bezoutlembz  12369  bezoutlembi  12370  bezoutlemle  12373  dfgcd3  12375  bezout  12376  dfgcd2  12379  dvdsmulgcd  12390  bezoutr  12397  uzwodc  12402  nninfctlemfo  12405  lcmval  12429  lcmcllem  12433  lcmneg  12440  ncoprmgcdne1b  12455  isprm2lem  12482  prmind2  12486  dvdsnprmd  12491  isprm5  12508  prmdvdsexp  12514  sqrt2irr  12528  oddpwdclemxy  12535  oddpwdclemdc  12539  nonsq  12573  pceu  12662  pcmul  12668  pc2dvds  12697  pcz  12699  pcprmpw2  12700  dvdsprmpweqle  12704  pcfac  12717  qexpz  12719  prmpwdvds  12722  1arith  12734  mul4sq  12761  4sqexercise2  12766  4sqlemsdc  12767  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemhom  12830  ennnfonelemfun  12832  ennnfonelemf1  12833  ennnfonelemim  12839  exmidunben  12841  ctiunctlemfo  12854  omiunct  12859  ssnnctlemct  12861  isstruct2r  12887  prdsval  13149  ismgm  13233  issgrp  13279  sgrppropd  13289  sgrpidmndm  13296  mndpropd  13316  issubmnd  13318  prdsidlem  13323  resmhm2b  13365  gsumwmhm  13374  isgrpinv  13430  grplmulf1o  13450  dfgrp3mlem  13474  grplactcnv  13478  pwssub  13489  mhmid  13495  mhmmnd  13496  ghmgrp  13498  mulgval  13502  mulgfng  13504  mulgnnp1  13510  mulgnn0dir  13532  mulgneg2  13536  mhmmulg  13543  grpissubg  13574  isnsg  13582  isnsg3  13587  nmzsubg  13590  ghmmhmb  13634  ghmpreima  13646  ghmnsgpreima  13649  ghmf1  13653  ghmf1o  13655  conjghm  13656  conjnmz  13659  conjnmzb  13660  ghmcmn  13707  gsumfzconst  13721  issrg  13771  srglmhm  13799  srgrmhm  13800  isring  13806  ringadd2  13833  ringlghm  13867  ringrghm  13868  oppr1g  13888  reldvdsrsrg  13898  dvdsrvald  13899  dvdsrd  13900  dvdsrex  13904  dvdsrmul1  13908  unitgrp  13922  rhmopp  13982  subrgintm  14049  subrgpropd  14059  isdomn  14075  lmodprop2d  14154  lssvacl  14171  lssvsubcl  14172  lssvscl  14181  lsslss  14187  lss1d  14189  lsspropdg  14237  expghmap  14413  mulgghm2  14414  znunit  14465  znrrg  14466  mplvalcoe  14496  mplsubgfilemcl  14505  mplsubgfileminv  14506  mplsubgfi  14507  opnssneib  14672  restbasg  14684  restopn2  14699  iscnp4  14734  cnss2  14743  cnconst2  14749  cnptopresti  14754  cnptoprest2  14756  neitx  14784  uptx  14790  txrest  14792  txdis1cn  14794  xmetres2  14895  xblss2ps  14920  blhalf  14924  blssps  14943  blss  14944  blssexps  14945  blssex  14946  blin2  14948  metequiv2  15012  bdmetval  15016  metcnp3  15027  metcnp  15028  metcn  15030  metcnpi  15031  metcnpi2  15032  txmetcnp  15034  txmetcn  15035  qtopbas  15038  tgqioo  15071  mpomulcn  15082  fsumcncntop  15083  elcncf2  15090  mulcncflem  15123  mulcncf  15124  suplociccreex  15140  limcdifap  15178  cnplimcim  15183  cnplimccntop  15186  limccnpcntop  15191  dvcj  15225  dvmptfsum  15241  dveflem  15242  ply1termlem  15258  plyaddlem1  15263  plymullem1  15264  plycolemc  15274  plycjlemc  15276  plyrecj  15279  dvply1  15281  reeff1olem  15287  eflt  15291  sin0pilem1  15297  ptolemy  15340  coseq0q4123  15350  coseq0negpitopi  15352  cos02pilt1  15367  cos11  15369  ioocosf1o  15370  rpcxpmul2  15429  cxplt  15432  cxple  15433  cxplt3  15436  apcxp2  15455  rprelogbmul  15471  rprelogbdiv  15473  dvdsppwf1o  15505  perfect  15517  lgsval  15525  lgsfcl2  15527  lgscllem  15528  lgsval2lem  15531  lgsdir2lem4  15552  lgsdir2lem5  15553  lgsdir2  15554  lgsne0  15559  gausslemma2dlem1a  15579  gausslemma2dlem1f1o  15581  2sqlem6  15641  2sqlem10  15646  2omap  16006  pwle2  16009  pwf1oexmid  16010  subctctexmid  16011  pw1nct  16014  peano4nninf  16017  nninfalllem1  16019  nninfall  16020  nninfsellemeq  16025  nninfsellemqall  16026  nnnninfex  16033  nninfnfiinf  16034  sbthom  16039  refeq  16041  isomninnlem  16043  trilpolemeq1  16053  trilpolemlt1  16054  trirec0  16057  apdiff  16061  iswomninnlem  16062  ismkvnnlem  16065  redcwlpolemeq1  16067  ltlenmkv  16083