Theorem 3simpa 984

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 970	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2	1	simplbi 272	1 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )

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

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 970

This theorem is referenced by:  3simpb  985  3simpc  986  simp1  987  simp2  988  3adant3  1007  3adantl3  1145  3adantr3  1148  opprc  3779  oprcl  3782  opm  4212  funtpg  5239  ftpg  5669  ovig  5963  prltlu  7428  mullocpr  7512  lt2halves  9092  nn0n0n1ge2  9261  ixxssixx  9838  sumtp  11355  dvdsmulcr  11761  dvds2add  11765  dvds2sub  11766  dvdstr  11768  bj-peano4  13837