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  3784  oprcl  3787  opm  4217  funtpg  5247  ftpg  5677  ovig  5971  prltlu  7436  mullocpr  7520  lt2halves  9100  nn0n0n1ge2  9269  ixxssixx  9846  sumtp  11364  dvdsmulcr  11770  dvds2add  11774  dvds2sub  11775  dvdstr  11777  bj-peano4  13950