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  5827  ovig  6132  prltlu  7685  mullocpr  7769  lt2halves  9358  nn0n0n1ge2  9528  ixxssixx  10110  pfxsuffeqwrdeq  11246  pfxccatpfx1  11284  pfxccatpfx2  11285  sumtp  11941  dvdsmulcr  12348  dvds2add  12352  dvds2sub  12353  dvdstr  12355  dfgrp3me  13649  wlkex  16071  wlkelwrd  16099  bj-peano4  16401