Theorem 3simpa 995

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

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

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 981

This theorem is referenced by:  3simpb  996  3simpc  997  simp1  998  simp2  999  3adant3  1018  3adantl3  1156  3adantr3  1159  opprc  3811  oprcl  3814  opm  4246  funtpg  5279  ftpg  5713  ovig  6010  prltlu  7500  mullocpr  7584  lt2halves  9168  nn0n0n1ge2  9337  ixxssixx  9916  sumtp  11436  dvdsmulcr  11842  dvds2add  11846  dvds2sub  11847  dvdstr  11849  dfgrp3me  12997  bj-peano4  15003