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  4132  nnsucelrlem3  4427  ltfintri  4467  ncfindi  4476  sfintfin  4533  vfintle  4547  phi11lem1  4596  fvopab4t  5386  xpassen  6058  nenpw1pwlem2  6086  ceclnn1  6190  spacssnc  6285  spaccl  6287  nchoicelem17  6306