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  3134  prepeano4  4451  preaddccan2  4455  tfin11  4493  tfinltfin  4501  evenodddisj  4516  sfindbl  4530  tfinnn  4534  vfinspsslem1  4550  vfinspclt  4552  xp0r  4842  weds  5938  ertr  5954  erth  5968  enadj  6060  enprmaplem3  6078  nntccl  6170  sbthlem3  6205  sbth  6206  tlecg  6230  nchoicelem6  6294  nchoicelem8  6296  nchoicelem19  6307  nchoice  6308