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  3800  oprcl  3803  opm  4235  funtpg  5268  ftpg  5701  ovig  5996  prltlu  7486  mullocpr  7570  lt2halves  9154  nn0n0n1ge2  9323  ixxssixx  9902  sumtp  11422  dvdsmulcr  11828  dvds2add  11832  dvds2sub  11833  dvdstr  11835  dfgrp3me  12970  bj-peano4  14710