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  4283  exmidundif  4291  exmidundifim  4292  frirrg  4442  reg2exmidlema  4627  imadiflem  5403  fvco4  5711  fvmptt  5731  fcoconst  5811  funopsn  5822  f1imass  5907  fcof1  5916  fliftfun  5929  riotass2  5992  ovmpodxf  6139  dftpos4  6420  tfrlem1  6465  tfrlem3ag  6466  tfrlemibacc  6483  tfrlemibfn  6485  tfrlemi1  6489  tfrlemi14d  6490  tfr1onlem3ag  6494  tfr1onlembacc  6499  tfr1onlembfn  6501  tfr1onlemaccex  6505  tfrcllembacc  6512  tfrcllembfn  6514  tfrcllemaccex  6518  frecabcl  6556  nntr2  6662  dcdifsnid  6663  nnm00  6689  ecopovsymg  6794  ecopoverg  6796  th3qlem1  6797  mapss  6851  f1imaen2g  6958  pw2f1odclem  7008  xpen  7019  xpmapenlem  7023  phpm  7040  fidifsnen  7045  dif1enen  7055  fiunsnnn  7056  fin0  7060  fin0or  7061  findcard2d  7066  findcard2sd  7067  diffifi  7069  isinfinf  7072  tridc  7075  fimax2gtrilemstep  7076  fimax2gtri  7077  en2eqpr  7085  onunsnss  7095  unsnfidcex  7098  unsnfidcel  7099  undifdcss  7101  unfiin  7104  fisseneq  7112  ssfirab  7114  f1finf1o  7130  fidcenumlemrks  7136  fidcenumlemrk  7137  fidcenumlemr  7138  fidcenum  7139  suplub2ti  7184  supisolem  7191  ordiso2  7218  djudom  7276  omp1eomlem  7277  difinfsnlem  7282  difinfinf  7284  ctm  7292  ctssdclemn0  7293  enumct  7298  nnnninfeq  7311  nnnninfeq2  7312  nninfisol  7316  enomnilem  7321  finomni  7323  exmidomni  7325  fodju0  7330  ismkvnex  7338  enmkvlem  7344  enwomnilem  7352  pr2cv1  7384  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidaclem  7406  exmidontriimlem1  7419  exmidontriimlem2  7420  exmidontriimlem3  7421  exmidontriimlem4  7422  exmidontriim  7423  netap  7456  exmidapne  7462  dfplpq2  7557  dfmpq2  7558  mulpipqqs  7576  nqpi  7581  distrnqg  7590  prarloclemarch  7621  enq0tr  7637  nqnq0pi  7641  nq0nn  7645  nnnq0lem1  7649  prarloclemup  7698  prarloclem3  7700  prarloclemcalc  7705  genplt2i  7713  addnqprllem  7730  addnqprulem  7731  appdivnq  7766  distrlem1prl  7785  distrlem1pru  7786  ltaddpr  7800  ltexprlemlol  7805  ltexprlemupu  7807  ltexprlemdisj  7809  addcanprleml  7817  ltaprlem  7821  addextpr  7824  recexprlemopu  7830  recexprlemdisj  7833  recexprlem1ssl  7836  aptiprleml  7842  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemlol  7850  cauappcvgprlemopu  7851  cauappcvgprlemdisj  7854  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemopu  7874  caucvgprlemladdfu  7880  caucvgprprlemml  7897  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemopu  7902  caucvgprprlemexbt  7909  suplocexprlemru  7922  suplocexprlemloc  7924  suplocexprlemub  7926  suplocexprlemlub  7927  prsrlem1  7945  recexgt0sr  7976  mulgt0sr  7981  archsr  7985  caucvgsrlemcau  7996  caucvgsrlemoffcau  8001  caucvgsrlemoffres  8003  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  addcnsr  8037  mulcnsr  8038  mulcnsrec  8046  axmulcom  8074  nntopi  8097  axcaucvglemcau  8101  axcaucvglemres  8102  axpre-suploclemres  8104  axpre-suploc  8105  mpomulf  8152  axsuploc  8235  ltntri  8290  cnegexlem2  8338  cnegexlem3  8339  addsub4  8405  le2add  8607  lt2add  8608  lt2sub  8623  le2sub  8624  rereim  8749  apreim  8766  mulreim  8767  apcotr  8770  apadd1  8771  addext  8773  mulext1  8775  mulext  8777  apti  8785  aptap  8813  receuap  8832  rec11rap  8874  divdivdivap  8876  divadddivap  8890  divsubdivap  8891  rerecclap  8893  recgt0  9013  prodgt0gt0  9014  prodgt0  9015  prodge0  9017  lemulge11  9029  lt2mul2div  9042  ltrec  9046  lerec  9047  ltrec1  9051  lediv2a  9058  mulle0r  9107  sup3exmid  9120  zdiv  9551  eluzuzle  9747  supinfneg  9807  infsupneg  9808  infregelbex  9810  xrltso  10009  xnn0dcle  10015  xnn0letri  10016  npnflt  10028  nmnfgt  10031  z2ge  10039  xaddf  10057  xaddval  10058  xpncan  10084  xleadd1a  10086  xltadd1  10089  xaddge0  10091  xle2add  10092  xleaddadd  10100  ixxss1  10117  ixxss2  10118  elico2  10150  iccsupr  10179  fzass4  10275  fzrev  10297  fz0fzelfz0  10340  fzocatel  10422  elfzomelpfzo  10454  zsupcllemstep  10466  exbtwnzlemstep  10484  rebtwn2zlemstep  10489  qbtwnxr  10494  xqltnle  10504  apbtwnz  10511  btwnzge0  10537  modqid  10588  modqcyc  10598  modqcyc2  10599  modqaddabs  10601  modqaddmod  10602  mulqaddmodid  10603  modqmuladd  10605  modqltm1p1mod  10615  modqsubmod  10621  modqsubmodmod  10622  modaddmodlo  10627  modqmulmod  10628  modqmulmodr  10629  modqsubdir  10632  addmodlteq  10637  nninfinf  10682  iseqf1olemab  10741  iseqf1olemmo  10744  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  seqf1oglem1  10758  seqf1oglem2  10759  seqf1og  10760  exp3val  10780  expcl2lemap  10790  expap0  10808  expnegzap  10812  expmul  10823  leexp1a  10833  qsqeqor  10889  expnbnd  10902  nn0ltexp2  10948  nn0opth2  10963  facndiv  10978  faclbnd  10980  bcval5  11002  bcpasc  11005  hashennnuni  11018  hashunlem  11043  hashunsng  11047  hashprg  11048  fiprsshashgt1  11057  hashxp  11066  fimaxq  11067  zfz1isolemiso  11079  zfz1isolem1  11080  seq3coll  11082  iswrdiz  11096  wrdnval  11120  ccatlen  11148  ccatvalfn  11154  ccatsymb  11155  ccatalpha  11166  swrdclg  11203  swrdsb0eq  11218  pfxwrdsymbg  11243  wrdind  11275  wrd2ind  11276  swrdccatin2  11282  pfxccatin12lem2  11284  pfxccatin12  11286  pfxccat3  11287  swrdccat  11288  shftlem  11348  shftfvalg  11350  shftfval  11353  2shfti  11363  caucvgrelemrec  11511  caucvgrelemcau  11512  caucvgre  11513  cvg1nlemcau  11516  cvg1nlemres  11517  resqrexlemcalc3  11548  resqrexlemcvg  11551  resqrexlemglsq  11554  resqrexlemga  11555  sqrtsq  11576  leabs  11606  absexpzap  11612  abslt  11620  absle  11621  abssubap0  11622  caubnd2  11649  icodiamlt  11712  maxleim  11737  maxabslemval  11740  maxleastlt  11747  rexico  11753  zmaxcl  11756  fimaxre2  11759  minmax  11762  xrmaxleim  11776  xrmaxiflemcl  11777  xrmaxifle  11778  xrmaxiflemlub  11780  xrmaxiflemval  11782  xrmaxleastlt  11788  xrmaxltsup  11790  xrmaxadd  11793  xrminmax  11797  xrbdtri  11808  climuni  11825  climshftlemg  11834  iserex  11871  climcau  11879  climrecvg1n  11880  climcvg1nlem  11881  sumeq2  11891  summodclem3  11912  zsumdc  11916  isumss  11923  fisumss  11924  sumsnf  11941  fsumconst  11986  modfsummod  11990  fsum00  11994  fsumabs  11997  fsumrelem  12003  fsumiun  12009  isumsplit  12023  divcnv  12029  geo2sum  12046  geoisumr  12050  cvgratz  12064  ntrivcvgap  12080  prodeq2  12089  prodmodclem2  12109  prodmodc  12110  zproddc  12111  fprodmul  12123  prodsnf  12124  fprodcl2lem  12137  fprodconst  12152  fprodap0  12153  fprodrec  12161  fprodap0f  12168  fprodle  12172  fprodmodd  12173  tanaddap  12271  zdvdsdc  12344  dvds2ln  12356  fsumdvds  12374  dvdsle  12376  dvdsext  12387  divalglemeunn  12453  divalglemex  12454  divalglemeuneg  12455  bitsfzo  12487  bitsmod  12488  bitsinv1lem  12493  bitsinv1  12494  dvdsbnd  12498  gcdsupex  12499  gcdsupcl  12500  dvdslegcd  12506  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlemzz  12544  bezoutlembz  12546  bezoutlembi  12547  bezoutlemle  12550  dfgcd3  12552  bezout  12553  dfgcd2  12556  dvdsmulgcd  12567  bezoutr  12574  uzwodc  12579  nninfctlemfo  12582  lcmval  12606  lcmcllem  12610  lcmneg  12617  ncoprmgcdne1b  12632  isprm2lem  12659  prmind2  12663  dvdsnprmd  12668  isprm5  12685  prmdvdsexp  12691  sqrt2irr  12705  oddpwdclemxy  12712  oddpwdclemdc  12716  nonsq  12750  pceu  12839  pcmul  12845  pc2dvds  12874  pcz  12876  pcprmpw2  12877  dvdsprmpweqle  12881  pcfac  12894  qexpz  12896  prmpwdvds  12899  1arith  12911  mul4sq  12938  4sqexercise2  12943  4sqlemsdc  12944  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemhom  13007  ennnfonelemfun  13009  ennnfonelemf1  13010  ennnfonelemim  13016  exmidunben  13018  ctiunctlemfo  13031  omiunct  13036  ssnnctlemct  13038  isstruct2r  13064  prdsval  13327  ismgm  13411  issgrp  13457  sgrppropd  13467  sgrpidmndm  13474  mndpropd  13494  issubmnd  13496  prdsidlem  13501  resmhm2b  13543  gsumwmhm  13552  isgrpinv  13608  grplmulf1o  13628  dfgrp3mlem  13652  grplactcnv  13656  pwssub  13667  mhmid  13673  mhmmnd  13674  ghmgrp  13676  mulgval  13680  mulgfng  13682  mulgnnp1  13688  mulgnn0dir  13710  mulgneg2  13714  mhmmulg  13721  grpissubg  13752  isnsg  13760  isnsg3  13765  nmzsubg  13768  ghmmhmb  13812  ghmpreima  13824  ghmnsgpreima  13827  ghmf1  13831  ghmf1o  13833  conjghm  13834  conjnmz  13837  conjnmzb  13838  ghmcmn  13885  gsumfzconst  13899  issrg  13949  srglmhm  13977  srgrmhm  13978  isring  13984  ringadd2  14011  ringlghm  14045  ringrghm  14046  oppr1g  14066  dvdsrvald  14078  dvdsrd  14079  dvdsrex  14083  dvdsrmul1  14087  unitgrp  14101  rhmopp  14161  subrgintm  14228  subrgpropd  14238  isdomn  14254  lmodprop2d  14333  lssvacl  14350  lssvsubcl  14351  lssvscl  14360  lsslss  14366  lss1d  14368  lsspropdg  14416  expghmap  14592  mulgghm2  14593  znunit  14644  znrrg  14645  mplvalcoe  14675  mplsubgfilemcl  14684  mplsubgfileminv  14685  mplsubgfi  14686  opnssneib  14851  restbasg  14863  restopn2  14878  iscnp4  14913  cnss2  14922  cnconst2  14928  cnptopresti  14933  cnptoprest2  14935  neitx  14963  uptx  14969  txrest  14971  txdis1cn  14973  xmetres2  15074  xblss2ps  15099  blhalf  15103  blssps  15122  blss  15123  blssexps  15124  blssex  15125  blin2  15127  metequiv2  15191  bdmetval  15195  metcnp3  15206  metcnp  15207  metcn  15209  metcnpi  15210  metcnpi2  15211  txmetcnp  15213  txmetcn  15214  qtopbas  15217  tgqioo  15250  mpomulcn  15261  fsumcncntop  15262  elcncf2  15269  mulcncflem  15302  mulcncf  15303  suplociccreex  15319  limcdifap  15357  cnplimcim  15362  cnplimccntop  15365  limccnpcntop  15370  dvcj  15404  dvmptfsum  15420  dveflem  15421  ply1termlem  15437  plyaddlem1  15442  plymullem1  15443  plycolemc  15453  plycjlemc  15455  plyrecj  15458  dvply1  15460  reeff1olem  15466  eflt  15470  sin0pilem1  15476  ptolemy  15519  coseq0q4123  15529  coseq0negpitopi  15531  cos02pilt1  15546  cos11  15548  ioocosf1o  15549  rpcxpmul2  15608  cxplt  15611  cxple  15612  cxplt3  15615  apcxp2  15634  rprelogbmul  15650  rprelogbdiv  15652  dvdsppwf1o  15684  perfect  15696  lgsval  15704  lgsfcl2  15706  lgscllem  15707  lgsval2lem  15710  lgsdir2lem4  15731  lgsdir2lem5  15732  lgsdir2  15733  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  2sqlem6  15820  2sqlem10  15825  umgrnloopv  15935  umgrvad2edg  16030  usgr1eop  16064  wlkvtxiedg  16117  wlkvtxiedgg  16118  upgredginwlk  16128  upgriswlkdc  16132  clwwlkccatlem  16169  pw1ndom3  16467  2omap  16472  pw1map  16474  pwle2  16477  pwf1oexmid  16478  subctctexmid  16479  pw1nct  16482  peano4nninf  16486  nninfalllem1  16488  nninfall  16489  nninfsellemeq  16494  nninfsellemqall  16495  nnnninfex  16502  nninfnfiinf  16503  sbthom  16508  refeq  16510  isomninnlem  16512  trilpolemeq1  16522  trilpolemlt1  16523  trirec0  16526  apdiff  16530  iswomninnlem  16531  ismkvnnlem  16534  redcwlpolemeq1  16536  ltlenmkv  16552