Theorem 3anass 982

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 980	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 401	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 184	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3anrot  983  3anan12  990  anandi3  991  3exdistr  1913  r3al  2519  ceqsex2  2775  ceqsex3v  2777  ceqsex4v  2778  ceqsex6v  2779  ceqsex8v  2780  eldifpr  3616  rexdifpr  3617  trel3  4104  sowlin  4314  dff1o4  5461  mpoxopovel  6232  dfsmo2  6278  ecopovtrn  6622  ecopovtrng  6625  elixp2  6692  elixp  6695  mptelixpg  6724  eqinfti  7009  distrnqg  7361  recmulnqg  7365  ltexnqq  7382  enq0tr  7408  distrnq0  7433  genpdflem  7481  distrlem1prl  7556  distrlem1pru  7557  divmulasscomap  8625  muldivdirap  8636  divmuldivap  8641  prime  9323  eluz2  9505  raluz2  9550  elixx1  9866  elixx3g  9870  elioo2  9890  elioo5  9902  elicc4  9909  iccneg  9958  icoshft  9959  elfz1  9982  elfz  9983  elfz2  9984  elfzm11  10059  elfz2nn0  10080  elfzo2  10118  elfzo3  10131  lbfzo0  10149  fzind2  10207  zmodid2  10320  redivap  10849  imdivap  10856  maxleast  11188  cosmul  11719  dfgcd2  11980  lcmneg  12039  coprmgcdb  12053  divgcdcoprmex  12067  cncongr1  12068  cncongr2  12069  difsqpwdvds  12302  elgz  12334  mgmsscl  12644  ismhm  12714  mhmpropd  12718  issubm  12724  issrg  12941  srglmhm  12969  srgrmhm  12970  isring  12976  lmbrf  13266  uptx  13325  txcn  13326  xmetec  13488  bl2ioo  13593  lgsmodeq  13997  lgsmulsqcoprm  13998  findset  14237