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  967  simp2lr  971  simp3lr  975  bilukdc  1284  intab  3635  imadiflem  4921  fvmptt  5205  fcoconst  5277  f1imass  5356  fcof1  5366  fliftfun  5379  riotass2  5437  ovmpt2dxf  5568  dftpos4  5819  tfrlem1  5864  tfrlem3ag  5865  tfrlemibacc  5881  tfrlemibfn  5883  tfrlemi1  5887  tfrlemi14d  5888  nnm00  6038  ecopovsymg  6141  ecopoverg  6143  th3qlem1  6144  f1imaen2g  6209  dfplpq2  6338  dfmpq2  6339  mulpipqqs  6357  nqpi  6362  distrnqg  6371  prarloclemarch  6401  enq0tr  6417  nqnq0pi  6421  nq0nn  6425  nnnq0lem1  6429  prarloclemup  6478  prarloclem3  6480  prarloclemcalc  6485  genplt2i  6493  addnqprllem  6510  addnqprulem  6511  appdivnq  6544  distrlem1prl  6558  distrlem1pru  6559  ltaddpr  6571  ltexprlemlol  6576  ltexprlemupu  6578  ltexprlemdisj  6580  addcanprleml  6588  ltaprlem  6591  addextpr  6593  recexprlemopu  6599  recexprlemdisj  6602  recexprlem1ssl  6605  aptiprleml  6611  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemdisj  6623  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemladdfu  6648  prsrlem1  6670  recexgt0sr  6701  mulgt0sr  6704  archsr  6708  addcnsr  6731  mulcnsr  6732  mulcnsrec  6740  axmulcom  6755  cnegexlem2  6984  cnegexlem3  6985  addsub4  7050  le2add  7234  lt2add  7235  lt2sub  7250  le2sub  7251  rereim  7370  apreim  7387  mulreim  7388  apcotr  7391  apadd1  7392  addext  7394  mulext1  7396  mulext  7398  apti  7406  receuap  7432  rec11rap  7469  divdivdivap  7471  divadddivap  7485  divsubdivap  7486  rerecclap  7488  recgt0  7597  prodgt0gt0  7598  prodgt0  7599  prodge0  7601  lemulge11  7613  lt2mul2div  7626  ltrec  7630  lerec  7631  ltrec1  7635  lediv2a  7642  zdiv  8104  eluzuzle  8257  xrltso  8487  z2ge  8509  ixxss1  8543  ixxss2  8544  elico2  8576  iccsupr  8605  fzass4  8695  fzrev  8716  fz0fzelfz0  8754  fzocatel  8825  elfzomelpfzo  8857  expival  8911  expcl2lemap  8921  expap0  8939  expnegzap  8943  expmul  8954  leexp1a  8963  expnbnd  9025  sqrtsq  9214