Theorem simprr 733

Description: Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)

Assertion

Ref	Expression
simprr	⊢ ((φ ∧ (ψ ∧ χ)) → χ)

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (χ → χ)
2	1	ad2antll 709	1 ⊢ ((φ ∧ (ψ ∧ χ)) → χ)

Syntax hints:   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  simp1rr  1021  simp2rr  1025  simp3rr  1029  prepeano4  4451  preaddccan2  4455  tfinltfin  4501  tfinnn  4534  vfinspsslem1  4550  weds  5938  ertr  5954  erth  5968  enadj  6060  enprmaplem3  6078  nntccl  6170  sbthlem1  6203  sbthlem3  6205  sbth  6206  tlecg  6230  nchoicelem6  6294  nchoicelem8  6296  nchoicelem19  6307  nchoice  6308