Theorem 3simpb 1059

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3simpb	|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ch ) )

Proof of Theorem 3simpb

Step	Hyp	Ref	Expression
1		3ancomb 1047	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ch /\ ps ) )
2		3simpa 1058	. 2 |- ( ( ph /\ ch /\ ps ) -> ( ph /\ ch ) )
3	1, 2	sylbi 207	1 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3adant2  1080  3adantl2  1218  3adantr2  1221  fpropnf1  6524  cfcof  9096  axcclem  9279  enqeq  9756  ltleletr  10130  ixxssixx  12189  prodmolem2  14665  prodmo  14666  zprod  14667  muldvds1  15006  dvds2add  15015  dvds2sub  15016  dvdstr  15018  initoeu2lem2  16665  pospropd  17134  csrgbinom  18546  smadiadetglem2  20478  ismbf3d  23421  mbfi1flimlem  23489  colinearalg  25790  frusgrnn0  26467  wlkwwlkinj  26782  2wlkond  26833  2pthond  26838  2pthon3v  26839  umgr2adedgwlkonALT  26843  usgr2wspthons3  26857  vdgn1frgrv2  27160  frgr2wwlkeqm  27195  extwwlkfab  27223  bnj967  31015  bnj1110  31050  cgr3permute3  32154  cgr3com  32160  brofs2  32184  areacirclem4  33503  paddasslem14  35119  lhpexle1  35294  cdlemk19w  36260  ismrc  37264  iocinico  37797  gneispb  38429  fourierdlem113  40436  sigaras  41044  sigarms  41045  leltletr  41308  lincresunit3lem3  42263  lincresunit3  42270