Theorem 3simpa 1021

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

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

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 1007

This theorem is referenced by:  3simpb  1022  3simpc  1023  simp1  1024  simp2  1025  3adant3  1044  3adantl3  1182  3adantr3  1185  opprc  3888  oprcl  3891  opm  4332  funtpg  5388  ftpg  5846  ovig  6153  prltlu  7767  mullocpr  7851  lt2halves  9439  nn0n0n1ge2  9611  ixxssixx  10198  pfxsuffeqwrdeq  11345  pfxccatpfx1  11383  pfxccatpfx2  11384  sumtp  12055  dvdsmulcr  12462  dvds2add  12466  dvds2sub  12467  dvdstr  12469  dfgrp3me  13763  uhgrissubgr  16202  subgrprop3  16203  0uhgrsubgr  16206  wlkex  16266  wlkelwrd  16294  bj-peano4  16671