Theorem 3anass 889

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

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

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 887	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 381	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 173	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 97   <-> wb 98   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3anrot  890  3anan12  897  anandi3  898  3exdistr  1792  r3al  2366  ceqsex2  2594  ceqsex3v  2596  ceqsex4v  2597  ceqsex6v  2598  ceqsex8v  2599  trel3  3862  sowlin  4057  dff1o4  5134  mpt2xopovel  5856  dfsmo2  5902  ecopovtrn  6203  ecopovtrng  6206  distrnqg  6485  recmulnqg  6489  ltexnqq  6506  enq0tr  6532  distrnq0  6557  genpdflem  6605  distrlem1prl  6680  distrlem1pru  6681  divmuldivap  7688  prime  8337  eluz2  8479  raluz2  8522  elixx1  8766  elixx3g  8770  elioo2  8790  elioo5  8802  elicc4  8809  iccneg  8857  icoshft  8858  elfz1  8879  elfz  8880  elfz2  8881  elfzm11  8953  elfz2nn0  8973  elfzo2  9007  elfzo3  9019  lbfzo0  9037  fzind2  9095  redivap  9474  imdivap  9481  findset  10070