Theorem 3simpa 1020

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

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

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 1006

This theorem is referenced by:  3simpb  1021  3simpc  1022  simp1  1023  simp2  1024  3adant3  1043  3adantl3  1181  3adantr3  1184  opprc  3883  oprcl  3886  opm  4326  funtpg  5381  ftpg  5838  ovig  6143  prltlu  7707  mullocpr  7791  lt2halves  9380  nn0n0n1ge2  9550  ixxssixx  10137  pfxsuffeqwrdeq  11283  pfxccatpfx1  11321  pfxccatpfx2  11322  sumtp  11993  dvdsmulcr  12400  dvds2add  12404  dvds2sub  12405  dvdstr  12407  dfgrp3me  13701  uhgrissubgr  16131  subgrprop3  16132  0uhgrsubgr  16135  wlkex  16195  wlkelwrd  16223  bj-peano4  16601