Theorem 3simpa 996

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

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

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 982

This theorem is referenced by:  3simpb  997  3simpc  998  simp1  999  simp2  1000  3adant3  1019  3adantl3  1157  3adantr3  1160  opprc  3826  oprcl  3829  opm  4264  funtpg  5306  ftpg  5743  ovig  6041  prltlu  7549  mullocpr  7633  lt2halves  9221  nn0n0n1ge2  9390  ixxssixx  9971  sumtp  11560  dvdsmulcr  11967  dvds2add  11971  dvds2sub  11972  dvdstr  11974  dfgrp3me  13175  bj-peano4  15517