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  2678  opkthg  4132  ltfintri  4467  ssfin  4471  foco2  5427  f1oiso2  5501  xpassen  6058  enadj  6061  lectr  6212