Theorem 3simpa 1018

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

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

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 1004

This theorem is referenced by:  3simpb  1019  3simpc  1020  simp1  1021  simp2  1022  3adant3  1041  3adantl3  1179  3adantr3  1182  opprc  3878  oprcl  3881  opm  4320  funtpg  5372  ftpg  5823  ovig  6126  prltlu  7674  mullocpr  7758  lt2halves  9347  nn0n0n1ge2  9517  ixxssixx  10098  pfxsuffeqwrdeq  11230  pfxccatpfx1  11268  pfxccatpfx2  11269  sumtp  11925  dvdsmulcr  12332  dvds2add  12336  dvds2sub  12337  dvdstr  12339  dfgrp3me  13633  wlkelwrd  16064  bj-peano4  16318