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  4279  funtpg  5326  ftpg  5770  ovig  6069  prltlu  7602  mullocpr  7686  lt2halves  9275  nn0n0n1ge2  9445  ixxssixx  10026  pfxsuffeqwrdeq  11152  sumtp  11758  dvdsmulcr  12165  dvds2add  12169  dvds2sub  12170  dvdstr  12172  dfgrp3me  13465  bj-peano4  15928