Theorem simprr 733

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

Assertion

Ref	Expression
simprr	|- ((ph /\ (ps /\ ch)) -> ch)

Proof of Theorem simprr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- (ch -> ch)
2	1	ad2antll 709	1 |- ((ph /\ (ps /\ ch)) -> ch)

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  4452  preaddccan2  4456  tfinltfin  4502  tfinnn  4535  vfinspsslem1  4551  weds  5939  ertr  5955  erth  5969  enadj  6061  enprmaplem3  6079  nntccl  6171  sbthlem1  6204  sbthlem3  6206  sbth  6207  tlecg  6231  nchoicelem6  6295  nchoicelem8  6297  nchoicelem19  6308  nchoice  6309