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  3830  oprcl  3833  opm  4268  funtpg  5310  ftpg  5749  ovig  6048  prltlu  7571  mullocpr  7655  lt2halves  9244  nn0n0n1ge2  9413  ixxssixx  9994  sumtp  11596  dvdsmulcr  12003  dvds2add  12007  dvds2sub  12008  dvdstr  12010  dfgrp3me  13302  bj-peano4  15685