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  3909  oprcl  3912  opm  4355  funtpg  5412  ftpg  5873  ovig  6183  prltlu  7818  mullocpr  7902  lt2halves  9491  nn0n0n1ge2  9665  ixxssixx  10254  pfxsuffeqwrdeq  11415  pfxccatpfx1  11453  pfxccatpfx2  11454  sumtp  12125  dvdsmulcr  12532  dvds2add  12536  dvds2sub  12537  dvdstr  12539  dfgrp3me  13855  uhgrissubgr  16382  subgrprop3  16383  0uhgrsubgr  16386  wlkex  16446  wlkelwrd  16474  bj-peano4  16851