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  1063  simp2lr  1067  simp3lr  1071  bilukdc  1407  dcun  3557  ifnefals  3600  intab  3900  exmid01  4228  exmidundif  4236  exmidundifim  4237  frirrg  4382  reg2exmidlema  4567  imadiflem  5334  fvco4  5630  fvmptt  5650  fcoconst  5730  f1imass  5818  fcof1  5827  fliftfun  5840  riotass2  5901  ovmpodxf  6045  dftpos4  6318  tfrlem1  6363  tfrlem3ag  6364  tfrlemibacc  6381  tfrlemibfn  6383  tfrlemi1  6387  tfrlemi14d  6388  tfr1onlem3ag  6392  tfr1onlembacc  6397  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfrcllembacc  6410  tfrcllembfn  6412  tfrcllemaccex  6416  frecabcl  6454  nntr2  6558  dcdifsnid  6559  nnm00  6585  ecopovsymg  6690  ecopoverg  6692  th3qlem1  6693  mapss  6747  f1imaen2g  6849  pw2f1odclem  6892  xpen  6903  xpmapenlem  6907  phpm  6923  fidifsnen  6928  dif1enen  6938  fiunsnnn  6939  fin0  6943  fin0or  6944  findcard2d  6949  findcard2sd  6950  diffifi  6952  isinfinf  6955  tridc  6957  fimax2gtrilemstep  6958  fimax2gtri  6959  en2eqpr  6965  onunsnss  6975  unsnfidcex  6978  unsnfidcel  6979  undifdcss  6981  unfiin  6984  fisseneq  6990  ssfirab  6992  f1finf1o  7008  fidcenumlemrks  7014  fidcenumlemrk  7015  fidcenumlemr  7016  fidcenum  7017  suplub2ti  7062  supisolem  7069  ordiso2  7096  djudom  7154  omp1eomlem  7155  difinfsnlem  7160  difinfinf  7162  ctm  7170  ctssdclemn0  7171  enumct  7176  nnnninfeq  7189  nnnninfeq2  7190  nninfisol  7194  enomnilem  7199  finomni  7201  exmidomni  7203  fodju0  7208  ismkvnex  7216  enmkvlem  7222  enwomnilem  7230  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  exmidontriimlem1  7283  exmidontriimlem2  7284  exmidontriimlem3  7285  exmidontriimlem4  7286  exmidontriim  7287  netap  7316  exmidapne  7322  dfplpq2  7416  dfmpq2  7417  mulpipqqs  7435  nqpi  7440  distrnqg  7449  prarloclemarch  7480  enq0tr  7496  nqnq0pi  7500  nq0nn  7504  nnnq0lem1  7508  prarloclemup  7557  prarloclem3  7559  prarloclemcalc  7564  genplt2i  7572  addnqprllem  7589  addnqprulem  7590  appdivnq  7625  distrlem1prl  7644  distrlem1pru  7645  ltaddpr  7659  ltexprlemlol  7664  ltexprlemupu  7666  ltexprlemdisj  7668  addcanprleml  7676  ltaprlem  7680  addextpr  7683  recexprlemopu  7689  recexprlemdisj  7692  recexprlem1ssl  7695  aptiprleml  7701  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemopu  7710  cauappcvgprlemdisj  7713  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemopu  7733  caucvgprlemladdfu  7739  caucvgprprlemml  7756  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemexbt  7768  suplocexprlemru  7781  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  prsrlem1  7804  recexgt0sr  7835  mulgt0sr  7840  archsr  7844  caucvgsrlemcau  7855  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  addcnsr  7896  mulcnsr  7897  mulcnsrec  7905  axmulcom  7933  nntopi  7956  axcaucvglemcau  7960  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  mpomulf  8011  axsuploc  8094  ltntri  8149  cnegexlem2  8197  cnegexlem3  8198  addsub4  8264  le2add  8465  lt2add  8466  lt2sub  8481  le2sub  8482  rereim  8607  apreim  8624  mulreim  8625  apcotr  8628  apadd1  8629  addext  8631  mulext1  8633  mulext  8635  apti  8643  aptap  8671  receuap  8690  rec11rap  8732  divdivdivap  8734  divadddivap  8748  divsubdivap  8749  rerecclap  8751  recgt0  8871  prodgt0gt0  8872  prodgt0  8873  prodge0  8875  lemulge11  8887  lt2mul2div  8900  ltrec  8904  lerec  8905  ltrec1  8909  lediv2a  8916  mulle0r  8965  sup3exmid  8978  zdiv  9408  eluzuzle  9603  supinfneg  9663  infsupneg  9664  infregelbex  9666  xrltso  9865  xnn0dcle  9871  xnn0letri  9872  npnflt  9884  nmnfgt  9887  z2ge  9895  xaddf  9913  xaddval  9914  xpncan  9940  xleadd1a  9942  xltadd1  9945  xaddge0  9947  xle2add  9948  xleaddadd  9956  ixxss1  9973  ixxss2  9974  elico2  10006  iccsupr  10035  fzass4  10131  fzrev  10153  fz0fzelfz0  10196  fzocatel  10269  elfzomelpfzo  10301  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  qbtwnxr  10329  xqltnle  10339  apbtwnz  10346  btwnzge0  10372  modqid  10423  modqcyc  10433  modqcyc2  10434  modqaddabs  10436  modqaddmod  10437  mulqaddmodid  10438  modqmuladd  10440  modqltm1p1mod  10450  modqsubmod  10456  modqsubmodmod  10457  modaddmodlo  10462  modqmulmod  10463  modqmulmodr  10464  modqsubdir  10467  addmodlteq  10472  nninfinf  10517  iseqf1olemab  10576  iseqf1olemmo  10579  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  seqf1oglem1  10593  seqf1oglem2  10594  seqf1og  10595  exp3val  10615  expcl2lemap  10625  expap0  10643  expnegzap  10647  expmul  10658  leexp1a  10668  qsqeqor  10724  expnbnd  10737  nn0ltexp2  10783  nn0opth2  10798  facndiv  10813  faclbnd  10815  bcval5  10837  bcpasc  10840  hashennnuni  10853  hashunlem  10878  hashunsng  10881  hashprg  10882  fiprsshashgt1  10891  hashxp  10900  fimaxq  10901  zfz1isolemiso  10913  zfz1isolem1  10914  seq3coll  10916  iswrdiz  10924  wrdnval  10947  shftlem  10963  shftfvalg  10965  shftfval  10968  2shfti  10978  caucvgrelemrec  11126  caucvgrelemcau  11127  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemcalc3  11163  resqrexlemcvg  11166  resqrexlemglsq  11169  resqrexlemga  11170  sqrtsq  11191  leabs  11221  absexpzap  11227  abslt  11235  absle  11236  abssubap0  11237  caubnd2  11264  icodiamlt  11327  maxleim  11352  maxabslemval  11355  maxleastlt  11362  rexico  11368  zmaxcl  11371  fimaxre2  11373  minmax  11376  xrmaxleim  11390  xrmaxiflemcl  11391  xrmaxifle  11392  xrmaxiflemlub  11394  xrmaxiflemval  11396  xrmaxleastlt  11402  xrmaxltsup  11404  xrmaxadd  11407  xrminmax  11411  xrbdtri  11422  climuni  11439  climshftlemg  11448  iserex  11485  climcau  11493  climrecvg1n  11494  climcvg1nlem  11495  sumeq2  11505  summodclem3  11526  zsumdc  11530  isumss  11537  fisumss  11538  sumsnf  11555  fsumconst  11600  modfsummod  11604  fsum00  11608  fsumabs  11611  fsumrelem  11617  fsumiun  11623  isumsplit  11637  divcnv  11643  geo2sum  11660  geoisumr  11664  cvgratz  11678  ntrivcvgap  11694  prodeq2  11703  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodmul  11737  prodsnf  11738  fprodcl2lem  11751  fprodconst  11766  fprodap0  11767  fprodrec  11775  fprodap0f  11782  fprodle  11786  fprodmodd  11787  tanaddap  11885  zdvdsdc  11958  dvds2ln  11970  dvdsle  11989  dvdsext  12000  divalglemeunn  12065  divalglemex  12066  divalglemeuneg  12067  zsupcllemstep  12085  dvdsbnd  12096  gcdsupex  12097  gcdsupcl  12098  dvdslegcd  12104  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlemzz  12142  bezoutlembz  12144  bezoutlembi  12145  bezoutlemle  12148  dfgcd3  12150  bezout  12151  dfgcd2  12154  dvdsmulgcd  12165  bezoutr  12172  uzwodc  12177  nninfctlemfo  12180  lcmval  12204  lcmcllem  12208  lcmneg  12215  ncoprmgcdne1b  12230  isprm2lem  12257  prmind2  12261  dvdsnprmd  12266  isprm5  12283  prmdvdsexp  12289  sqrt2irr  12303  oddpwdclemxy  12310  oddpwdclemdc  12314  nonsq  12348  pceu  12436  pcmul  12442  pc2dvds  12471  pcz  12473  pcprmpw2  12474  dvdsprmpweqle  12478  pcfac  12491  qexpz  12493  prmpwdvds  12496  1arith  12508  mul4sq  12535  4sqexercise2  12540  4sqlemsdc  12541  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemhom  12575  ennnfonelemfun  12577  ennnfonelemf1  12578  ennnfonelemim  12584  exmidunben  12586  ctiunctlemfo  12599  omiunct  12604  ssnnctlemct  12606  isstruct2r  12632  ismgm  12943  issgrp  12989  sgrppropd  12999  sgrpidmndm  13004  mndpropd  13024  issubmnd  13026  resmhm2b  13064  gsumwmhm  13073  isgrpinv  13129  grplmulf1o  13149  dfgrp3mlem  13173  grplactcnv  13177  mhmid  13188  mhmmnd  13189  ghmgrp  13191  mulgval  13195  mulgfng  13197  mulgnnp1  13203  mulgnn0dir  13225  mulgneg2  13229  mhmmulg  13236  grpissubg  13267  isnsg  13275  isnsg3  13280  nmzsubg  13283  ghmmhmb  13327  ghmpreima  13339  ghmnsgpreima  13342  ghmf1  13346  ghmf1o  13348  conjghm  13349  conjnmz  13352  conjnmzb  13353  ghmcmn  13400  gsumfzconst  13414  issrg  13464  srglmhm  13492  srgrmhm  13493  isring  13499  ringadd2  13526  ringlghm  13560  ringrghm  13561  oppr1g  13581  reldvdsrsrg  13591  dvdsrvald  13592  dvdsrd  13593  dvdsrex  13597  dvdsrmul1  13601  unitgrp  13615  rhmopp  13675  subrgintm  13742  subrgpropd  13752  isdomn  13768  lmodprop2d  13847  lssvacl  13864  lssvsubcl  13865  lssvscl  13874  lsslss  13880  lss1d  13882  lsspropdg  13930  expghmap  14106  mulgghm2  14107  znunit  14158  znrrg  14159  opnssneib  14335  restbasg  14347  restopn2  14362  iscnp4  14397  cnss2  14406  cnconst2  14412  cnptopresti  14417  cnptoprest2  14419  neitx  14447  uptx  14453  txrest  14455  txdis1cn  14457  xmetres2  14558  xblss2ps  14583  blhalf  14587  blssps  14606  blss  14607  blssexps  14608  blssex  14609  blin2  14611  metequiv2  14675  bdmetval  14679  metcnp3  14690  metcnp  14691  metcn  14693  metcnpi  14694  metcnpi2  14695  txmetcnp  14697  txmetcn  14698  qtopbas  14701  tgqioo  14734  mpomulcn  14745  fsumcncntop  14746  elcncf2  14753  mulcncflem  14786  mulcncf  14787  suplociccreex  14803  limcdifap  14841  cnplimcim  14846  cnplimccntop  14849  limccnpcntop  14854  dvcj  14888  dvmptfsum  14904  dveflem  14905  ply1termlem  14921  plyaddlem1  14926  plymullem1  14927  plycolemc  14936  plycjlemc  14938  plyrecj  14941  dvply1  14943  reeff1olem  14947  eflt  14951  sin0pilem1  14957  ptolemy  15000  coseq0q4123  15010  coseq0negpitopi  15012  cos02pilt1  15027  cos11  15029  ioocosf1o  15030  cxplt  15091  cxple  15092  cxplt3  15095  apcxp2  15113  rprelogbmul  15128  rprelogbdiv  15130  lgsval  15161  lgsfcl2  15163  lgscllem  15164  lgsval2lem  15167  lgsdir2lem4  15188  lgsdir2lem5  15189  lgsdir2  15190  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  2sqlem6  15277  2sqlem10  15282  pwle2  15559  pwf1oexmid  15560  subctctexmid  15561  pw1nct  15563  peano4nninf  15566  nninfalllem1  15568  nninfall  15569  nninfsellemeq  15574  nninfsellemqall  15575  sbthom  15586  refeq  15588  isomninnlem  15590  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  apdiff  15608  iswomninnlem  15609  ismkvnnlem  15612  redcwlpolemeq1  15614  ltlenmkv  15630