Theorem 3simpa 994

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

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3simpb  995  3simpc  996  simp1  997  simp2  998  3adant3  1017  3adantl3  1155  3adantr3  1158  opprc  3799  oprcl  3802  opm  4234  funtpg  5267  ftpg  5700  ovig  5995  prltlu  7485  mullocpr  7569  lt2halves  9153  nn0n0n1ge2  9322  ixxssixx  9901  sumtp  11421  dvdsmulcr  11827  dvds2add  11831  dvds2sub  11832  dvdstr  11834  dfgrp3me  12969  bj-peano4  14677