Theorem 3anass 949

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 947	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 396	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 183	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 103   <-> wb 104   /\ w3a 945

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  3anrot  950  3anan12  957  anandi3  958  3exdistr  1867  r3al  2451  ceqsex2  2697  ceqsex3v  2699  ceqsex4v  2700  ceqsex6v  2701  ceqsex8v  2702  trel3  3994  sowlin  4202  dff1o4  5331  mpoxopovel  6092  dfsmo2  6138  ecopovtrn  6480  ecopovtrng  6483  elixp2  6550  elixp  6553  mptelixpg  6582  eqinfti  6859  distrnqg  7143  recmulnqg  7147  ltexnqq  7164  enq0tr  7190  distrnq0  7215  genpdflem  7263  distrlem1prl  7338  distrlem1pru  7339  divmulasscomap  8369  muldivdirap  8380  divmuldivap  8385  prime  9054  eluz2  9234  raluz2  9276  elixx1  9573  elixx3g  9577  elioo2  9597  elioo5  9609  elicc4  9616  iccneg  9665  icoshft  9666  elfz1  9688  elfz  9689  elfz2  9690  elfzm11  9764  elfz2nn0  9785  elfzo2  9820  elfzo3  9833  lbfzo0  9851  fzind2  9909  zmodid2  10018  redivap  10539  imdivap  10546  maxleast  10877  cosmul  11303  dfgcd2  11548  lcmneg  11601  coprmgcdb  11615  divgcdcoprmex  11629  cncongr1  11630  cncongr2  11631  lmbrf  12226  uptx  12285  txcn  12286  xmetec  12426  bl2ioo  12528  findset  12835