Theorem simplr 482

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 458	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  simp1lr  968  simp2lr  972  simp3lr  976  bilukdc  1287  intab  3644  frirrg  4087  reg2exmidlema  4259  imadiflem  4978  fvmptt  5262  fcoconst  5334  f1imass  5413  fcof1  5423  fliftfun  5436  riotass2  5494  ovmpt2dxf  5626  dftpos4  5878  tfrlem1  5923  tfrlem3ag  5924  tfrlemibacc  5940  tfrlemibfn  5942  tfrlemi1  5946  tfrlemi14d  5947  nndifsnid  6080  nnm00  6102  ecopovsymg  6205  ecopoverg  6207  th3qlem1  6208  f1imaen2g  6273  phpm  6327  fidifsnen  6331  fidifsnid  6332  fiunsnnn  6338  fin0  6342  fin0or  6343  findcard2d  6348  findcard2sd  6349  diffifi  6351  onunsnss  6355  ordiso2  6357  dfplpq2  6452  dfmpq2  6453  mulpipqqs  6471  nqpi  6476  distrnqg  6485  prarloclemarch  6516  enq0tr  6532  nqnq0pi  6536  nq0nn  6540  nnnq0lem1  6544  prarloclemup  6593  prarloclem3  6595  prarloclemcalc  6600  genplt2i  6608  addnqprllem  6625  addnqprulem  6626  appdivnq  6661  distrlem1prl  6680  distrlem1pru  6681  ltaddpr  6695  ltexprlemlol  6700  ltexprlemupu  6702  ltexprlemdisj  6704  addcanprleml  6712  ltaprlem  6716  addextpr  6719  recexprlemopu  6725  recexprlemdisj  6728  recexprlem1ssl  6731  aptiprleml  6737  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemdisj  6749  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemladdfu  6775  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemexbt  6804  prsrlem1  6827  recexgt0sr  6858  mulgt0sr  6862  archsr  6866  caucvgsrlemcau  6877  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  addcnsr  6910  mulcnsr  6911  mulcnsrec  6919  axmulcom  6945  nntopi  6968  axcaucvglemcau  6972  axcaucvglemres  6973  cnegexlem2  7187  cnegexlem3  7188  addsub4  7254  le2add  7439  lt2add  7440  lt2sub  7455  le2sub  7456  rereim  7577  apreim  7594  mulreim  7595  apcotr  7598  apadd1  7599  addext  7601  mulext1  7603  mulext  7605  apti  7613  receuap  7650  rec11rap  7687  divdivdivap  7689  divadddivap  7703  divsubdivap  7704  rerecclap  7706  recgt0  7816  prodgt0gt0  7817  prodgt0  7818  prodge0  7820  lemulge11  7832  lt2mul2div  7845  ltrec  7849  lerec  7850  ltrec1  7854  lediv2a  7861  zdiv  8328  eluzuzle  8481  xrltso  8717  z2ge  8739  ixxss1  8773  ixxss2  8774  elico2  8806  iccsupr  8835  fzass4  8925  fzrev  8946  fz0fzelfz0  8984  fzocatel  9055  elfzomelpfzo  9087  rebtwn2zlemstep  9107  btwnzge0  9142  expival  9257  expcl2lemap  9267  expap0  9285  expnegzap  9289  expmul  9300  leexp1a  9309  expnbnd  9372  shftlem  9417  shftfvalg  9419  shftfval  9422  2shfti  9432  caucvgrelemrec  9578  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemcalc3  9614  resqrexlemcvg  9617  resqrexlemglsq  9620  resqrexlemga  9621  sqrtsq  9642  leabs  9672  absexpzap  9676  abslt  9684  absle  9685  abssubap0  9686  caubnd2  9713  icodiamlt  9776  climuni  9814  climshftlemg  9823  iiserex  9859  climcau  9866  climrecvg1n  9867  climcvg1nlem  9868  sqrt2irr  9878