Theorem 3simpa 997

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

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

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 983

This theorem is referenced by:  3simpb  998  3simpc  999  simp1  1000  simp2  1001  3adant3  1020  3adantl3  1158  3adantr3  1161  opprc  3854  oprcl  3857  opm  4296  funtpg  5344  ftpg  5791  ovig  6090  prltlu  7635  mullocpr  7719  lt2halves  9308  nn0n0n1ge2  9478  ixxssixx  10059  pfxsuffeqwrdeq  11189  pfxccatpfx1  11227  pfxccatpfx2  11228  sumtp  11840  dvdsmulcr  12247  dvds2add  12251  dvds2sub  12252  dvdstr  12254  dfgrp3me  13547  bj-peano4  16090