Theorem simplr 470

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 462	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  954  simp2lr  958  simp3lr  962  bilukdc  1268  intab  3614  imadiflem  4900  fvmptt  5183  fcoconst  5255  f1imass  5334  fcof1  5344  fliftfun  5357  riotass2  5414  ovmpt2dxf  5545  dftpos4  5796  tfrlem1  5841  tfrlem3ag  5842  tfrlemibacc  5857  tfrlemibfn  5859  tfrlemi1  5863  tfrlemi14d  5864  nnm00  6009  ecopovsymg  6112  ecopoverg  6114  th3qlem1  6115  dfplpq2  6207  dfmpq2  6208  mulpipqqs  6226  nqpi  6231  distrnqg  6240  prarloclemarch  6269  enq0tr  6283  nqnq0pi  6287  nq0nn  6291  nnnq0lem1  6295  prarloclemup  6343  prarloclem3  6345  prarloclemcalc  6350  genplt2i  6358  addnqprllem  6376  addnqprulem  6377  appdivnq  6401  distrlem1prl  6415  distrlem1pru  6416  ltaddpr  6428  ltexprlemlol  6433  ltexprlemupu  6435  ltexprlemdisj  6437  addcanprleml  6445  ltaprlem  6448  recexprlemopu  6455  recexprlemdisj  6458  recexprlem1ssl  6461  aptiprleml  6467  prsrlem1  6486  recexgt0sr  6517  mulgt0sr  6520  addcnsr  6544  mulcnsr  6545  mulcnsrec  6553  axmulcom  6564  cnegexlem2  6789  cnegexlem3  6790  addsub4  6855  le2add  7039  lt2add  7040  lt2sub  7055  le2sub  7056  rereim  7175  apreim  7188  apcotr  7191  apadd1  7192  extadd  7194