Theorem 3simpa 989

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

Assertion

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

Proof of Theorem 3simpa

Step	Hyp	Ref	Expression
1		df-3an 975	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2	1	simplbi 272	1 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3simpb  990  3simpc  991  simp1  992  simp2  993  3adant3  1012  3adantl3  1150  3adantr3  1153  opprc  3786  oprcl  3789  opm  4219  funtpg  5249  ftpg  5680  ovig  5974  prltlu  7449  mullocpr  7533  lt2halves  9113  nn0n0n1ge2  9282  ixxssixx  9859  sumtp  11377  dvdsmulcr  11783  dvds2add  11787  dvds2sub  11788  dvdstr  11790  bj-peano4  13990