Theorem 3simpa 1025

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

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

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 1011

This theorem is referenced by:  3simpb  1026  3simpc  1027  simp1  1028  simp2  1029  3adant3  1048  3adantl3  1186  3adantr3  1189  opprc  3920  oprcl  3923  opm  4369  funtpg  5427  ftpg  5890  ovig  6200  prltlu  7844  mullocpr  7928  lt2halves  9520  nn0n0n1ge2  9694  ixxssixx  10283  pfxsuffeqwrdeq  11448  pfxccatpfx1  11486  pfxccatpfx2  11487  sumtp  12159  dvdsmulcr  12566  dvds2add  12570  dvds2sub  12571  dvdstr  12573  dfgrp3me  13882  uhgrissubgr  16416  subgrprop3  16417  0uhgrsubgr  16420  wlkex  16480  wlkelwrd  16508  bj-peano4  16895