Theorem simp3 957

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

Assertion

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

Proof of Theorem simp3

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

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:  simpl3  960  simpr3  963  simp3i  966  simp3d  969  simp13  987  simp23  990  simp33  993  3anibar  1123  mob2  3017  opkthg  4132  ncfindi  4476  tfindi  4497  nnadjoinpw  4522  sfintfin  4533  tfinnn  4535  vfintle  4547  peano4  4558  fvopab4t  5386  f1oiso2  5501  ov2ag  5599  xpassen  6058  nenpw1pwlem2  6086  ceclnn1  6190  nclenc  6223  lenc  6224  taddc  6230  addcdir  6252  spaccl  6287