Theorem simp1 955

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

Assertion

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

Proof of Theorem simp1

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

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:  simpl1  958  simpr1  961  simp1i  964  simp1d  967  simp11  985  simp21  988  simp31  991  syld3an3  1227  rsp2e  2677  opkthg  4131  ltfintri  4466  ssfin  4470  foco2  5426  f1oiso2  5500  xpassen  6057  enadj  6060  lectr  6211