Theorem simplr 731

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

Assertion

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

Proof of Theorem simplr

Step	Hyp	Ref	Expression
1		id 19	. 2 |- (ps -> ps)
2	1	ad2antlr 707	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:  simp1lr  1019  simp2lr  1023  simp3lr  1027  ax11indalem  2197  ax11inda2ALT  2198  ifboth  3693  intab  3956  prepeano4  4451  leltfintr  4458  lenltfin  4469  tfinnn  4534  phi11lem1  4595  imainss  5042  ncssfin  6151  nntccl  6170  sbth  6206  leconnnc  6218  tlecg  6230  lemuc1  6253  ncslesuc  6267  spacind  6287  nchoicelem8  6296  nchoicelem19  6307  nchoice  6308  fnfrec  6320