Theorem 3simpa 997

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

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

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 983

This theorem is referenced by:  3simpb  998  3simpc  999  simp1  1000  simp2  1001  3adant3  1020  3adantl3  1158  3adantr3  1161  opprc  3840  oprcl  3843  opm  4278  funtpg  5325  ftpg  5768  ovig  6067  prltlu  7600  mullocpr  7684  lt2halves  9273  nn0n0n1ge2  9443  ixxssixx  10024  sumtp  11725  dvdsmulcr  12132  dvds2add  12136  dvds2sub  12137  dvdstr  12139  dfgrp3me  13432  bj-peano4  15891