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  6416  nqnq0pi  6420  nq0nn  6424  nnnq0lem1  6428  prarloclemup  6477  prarloclem3  6479  prarloclemcalc  6484  genplt2i  6492  addnqprllem  6509  addnqprulem  6510  appdivnq  6543  distrlem1prl  6557  distrlem1pru  6558  ltaddpr  6570  ltexprlemlol  6575  ltexprlemupu  6577  ltexprlemdisj  6579  addcanprleml  6587  ltaprlem  6590  addextpr  6592  recexprlemopu  6598  recexprlemdisj  6601  recexprlem1ssl  6604  aptiprleml  6610  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemopu  6619  cauappcvgprlemdisj  6622  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  prsrlem1  6650  recexgt0sr  6681  mulgt0sr  6684  archsr  6688  addcnsr  6711  mulcnsr  6712  mulcnsrec  6720  axmulcom  6735  cnegexlem2  6964  cnegexlem3  6965  addsub4  7030  le2add  7214  lt2add  7215  lt2sub  7230  le2sub  7231  rereim  7350  apreim  7367  mulreim  7368  apcotr  7371  apadd1  7372  addext  7374  mulext1  7376  mulext  7378  apti  7386  receuap  7412  rec11rap  7449  divdivdivap  7451  divadddivap  7465  divsubdivap  7466  rerecclap  7468  recgt0  7577  prodgt0gt0  7578  prodgt0  7579  prodge0  7581  lemulge11  7593  lt2mul2div  7606  ltrec  7610  lerec  7611  ltrec1  7615  lediv2a  7622  zdiv  8084  eluzuzle  8237  xrltso  8467  z2ge  8489  ixxss1  8523  ixxss2  8524  elico2  8556  iccsupr  8585  fzass4  8675  fzrev  8696  fz0fzelfz0  8734  fzocatel  8805  elfzomelpfzo  8837  expival  8891  expcl2lemap  8901  expap0  8919  expnegzap  8923  expmul  8934  leexp1a  8943  expnbnd  9005  sqrtsq  9194