Theorem simp2 956

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

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

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 952	. 2 |- ((ph /\ ps /\ ch) -> (ph /\ ps))
2	1	simprd 449	1 |- ((ph /\ ps /\ ch) -> ps)

Syntax hints:   -> wi 4   /\ w3a 934

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  df-3an 936

This theorem is referenced by:  simpl2  959  simpr2  962  simp2i  965  simp2d  968  simp12  986  simp22  989  simp32  992  syld3an3  1227  opkthg  4131  nnsucelrlem3  4426  ltfintri  4466  ncfindi  4475  sfintfin  4532  vfintle  4546  phi11lem1  4595  fvopab4t  5385  xpassen  6057  nenpw1pwlem2  6085  ceclnn1  6189  spacssnc  6284  spaccl  6286  nchoicelem17  6305