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  3694  intab  3957  prepeano4  4452  leltfintr  4459  lenltfin  4470  tfinnn  4535  phi11lem1  4596  imainss  5043  ncssfin  6152  nntccl  6171  sbth  6207  leconnnc  6219  tlecg  6231  lemuc1  6254  ncslesuc  6268  spacind  6288  nchoicelem8  6297  nchoicelem19  6308  nchoice  6309  fnfrec  6321