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  3825  oprcl  3828  opm  4263  funtpg  5305  ftpg  5742  ovig  6040  prltlu  7547  mullocpr  7631  lt2halves  9218  nn0n0n1ge2  9387  ixxssixx  9968  sumtp  11557  dvdsmulcr  11964  dvds2add  11968  dvds2sub  11969  dvdstr  11971  dfgrp3me  13172  bj-peano4  15447