Theorem 3anass 923

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 921	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 393	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 182	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 102   <-> wb 103   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3anrot  924  3anan12  931  anandi3  932  3exdistr  1833  r3al  2408  ceqsex2  2639  ceqsex3v  2641  ceqsex4v  2642  ceqsex6v  2643  ceqsex8v  2644  trel3  3883  sowlin  4075  dff1o4  5154  mpt2xopovel  5879  dfsmo2  5925  ecopovtrn  6226  ecopovtrng  6229  eqinfti  6433  distrnqg  6577  recmulnqg  6581  ltexnqq  6598  enq0tr  6624  distrnq0  6649  genpdflem  6697  distrlem1prl  6772  distrlem1pru  6773  divmulasscomap  7784  muldivdirap  7795  divmuldivap  7800  prime  8446  eluz2  8625  raluz2  8667  elixx1  8920  elixx3g  8924  elioo2  8944  elioo5  8956  elicc4  8963  iccneg  9011  icoshft  9012  elfz1  9034  elfz  9035  elfz2  9036  elfzm11  9108  elfz2nn0  9128  elfzo2  9160  elfzo3  9172  lbfzo0  9190  fzind2  9248  zmodid2  9354  redivap  9761  imdivap  9768  maxleast  10099  dfgcd2  10403  lcmneg  10456  coprmgcdb  10470  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  findset  10740