Theorem simplr 496

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

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  simp1lr  1002  simp2lr  1006  simp3lr  1010  bilukdc  1327  intab  3665  frirrg  4105  reg2exmidlema  4277  imadiflem  4998  fvmptt  5283  fcoconst  5355  f1imass  5434  fcof1  5443  fliftfun  5456  riotass2  5514  ovmpt2dxf  5646  dftpos4  5901  tfrlem1  5946  tfrlem3ag  5947  tfrlemibacc  5963  tfrlemibfn  5965  tfrlemi1  5969  tfrlemi14d  5970  nndifsnid  6103  nnm00  6125  ecopovsymg  6228  ecopoverg  6230  th3qlem1  6231  f1imaen2g  6296  phpm  6351  fidifsnen  6355  fidifsnid  6356  fiunsnnn  6365  fin0  6369  fin0or  6370  findcard2d  6375  findcard2sd  6376  diffifi  6378  en2eqpr  6380  onunsnss  6383  unsnfidcex  6385  unsnfidcel  6386  suplub2ti  6414  supisolem  6421  ordiso2  6446  dfplpq2  6544  dfmpq2  6545  mulpipqqs  6563  nqpi  6568  distrnqg  6577  prarloclemarch  6608  enq0tr  6624  nqnq0pi  6628  nq0nn  6632  nnnq0lem1  6636  prarloclemup  6685  prarloclem3  6687  prarloclemcalc  6692  genplt2i  6700  addnqprllem  6717  addnqprulem  6718  appdivnq  6753  distrlem1prl  6772  distrlem1pru  6773  ltaddpr  6787  ltexprlemlol  6792  ltexprlemupu  6794  ltexprlemdisj  6796  addcanprleml  6804  ltaprlem  6808  addextpr  6811  recexprlemopu  6817  recexprlemdisj  6820  recexprlem1ssl  6823  aptiprleml  6829  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemladdfu  6867  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemexbt  6896  prsrlem1  6919  recexgt0sr  6950  mulgt0sr  6954  archsr  6958  caucvgsrlemcau  6969  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  addcnsr  7002  mulcnsr  7003  mulcnsrec  7011  axmulcom  7037  nntopi  7060  axcaucvglemcau  7064  axcaucvglemres  7065  cnegexlem2  7284  cnegexlem3  7285  addsub4  7351  le2add  7548  lt2add  7549  lt2sub  7564  le2sub  7565  rereim  7686  apreim  7703  mulreim  7704  apcotr  7707  apadd1  7708  addext  7710  mulext1  7712  mulext  7714  apti  7722  receuap  7759  rec11rap  7799  divdivdivap  7801  divadddivap  7815  divsubdivap  7816  rerecclap  7818  recgt0  7928  prodgt0gt0  7929  prodgt0  7930  prodge0  7932  lemulge11  7944  lt2mul2div  7957  ltrec  7961  lerec  7962  ltrec1  7966  lediv2a  7973  mulle0r  8022  zdiv  8435  eluzuzle  8627  supinfneg  8683  infsupneg  8684  xrltso  8871  z2ge  8893  ixxss1  8927  ixxss2  8928  elico2  8960  iccsupr  8989  fzass4  9080  fzrev  9101  fz0fzelfz0  9138  fzocatel  9208  elfzomelpfzo  9240  rebtwn2zlemstep  9261  qbtwnxr  9266  btwnzge0  9302  modqid  9351  modqcyc  9361  modqcyc2  9362  modqaddabs  9364  modqaddmod  9365  mulqaddmodid  9366  modqmuladd  9368  modqltm1p1mod  9378  modqsubmod  9384  modqsubmodmod  9385  modaddmodlo  9390  modqmulmod  9391  modqmulmodr  9392  modqsubdir  9395  addmodlteq  9400  expival  9478  expcl2lemap  9488  expap0  9506  expnegzap  9510  expmul  9521  leexp1a  9531  expnbnd  9596  nn0opth2  9651  facndiv  9666  faclbnd  9668  ibcval5  9690  bcpasc  9693  shftlem  9704  shftfvalg  9706  shftfval  9709  2shfti  9719  caucvgrelemrec  9865  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemcalc3  9902  resqrexlemcvg  9905  resqrexlemglsq  9908  resqrexlemga  9909  sqrtsq  9930  leabs  9960  absexpzap  9966  abslt  9974  absle  9975  abssubap0  9976  caubnd2  10003  icodiamlt  10066  maxleim  10091  maxabslemval  10094  maxleastlt  10101  rexico  10107  fimaxre2  10109  minmax  10112  climuni  10132  climshftlemg  10141  iiserex  10177  climcau  10184  climrecvg1n  10185  climcvg1nlem  10186  zdvdsdc  10216  dvds2ln  10228  dvdsle  10244  dvdsext  10255  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  zsupcllemstep  10341  dvdsbnd  10348  gcdsupex  10349  gcdsupcl  10350  dvdslegcd  10356  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemzz  10391  bezoutlembz  10393  bezoutlembi  10394  bezoutlemle  10397  dfgcd3  10399  bezout  10400  dfgcd2  10403  dvdsmulgcd  10414  bezoutr  10421  lcmval  10445  lcmcllem  10449  lcmneg  10456  ncoprmgcdne1b  10471  isprm2lem  10498  prmind2  10502  dvdsnprmd  10507  prmdvdsexp  10527  sqrt2irr  10541  oddpwdclemxy  10547  oddpwdclemdc  10551