Theorem simprl 732

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

Assertion

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

Proof of Theorem simprl

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

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:  simp1rl  1020  simp2rl  1024  simp3rl  1028  rmob  3135  prepeano4  4452  preaddccan2  4456  tfin11  4494  tfinltfin  4502  evenodddisj  4517  sfindbl  4531  tfinnn  4535  vfinspsslem1  4551  vfinspclt  4553  xp0r  4843  weds  5939  ertr  5955  erth  5969  enadj  6061  enprmaplem3  6079  nntccl  6171  sbthlem3  6206  sbth  6207  tlecg  6231  nchoicelem6  6295  nchoicelem8  6297  nchoicelem19  6308  nchoice  6309