Theorem 3anass 1008

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 1006	. 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 1004

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 1006

This theorem is referenced by:  3anrot  1009  3anan12  1016  anandi3  1017  3biant1d  1391  3exdistr  1964  r3al  2576  ceqsex2  2844  ceqsex3v  2846  ceqsex4v  2847  ceqsex6v  2848  ceqsex8v  2849  eldifpr  3696  rexdifpr  3697  trel3  4195  sowlin  4417  dff1o4  5591  mpoxopovel  6407  dfsmo2  6453  ecopovtrn  6801  ecopovtrng  6804  elixp2  6871  elixp  6874  mptelixpg  6903  eqinfti  7219  distrnqg  7607  recmulnqg  7611  ltexnqq  7628  enq0tr  7654  distrnq0  7679  genpdflem  7727  distrlem1prl  7802  distrlem1pru  7803  divmulasscomap  8876  muldivdirap  8887  divmuldivap  8892  prime  9579  eluz2  9761  raluz2  9813  elixx1  10132  elixx3g  10136  elioo2  10156  elioo5  10168  elicc4  10175  iccneg  10224  icoshft  10225  elfz1  10248  elfz  10249  elfz2  10250  elfzm11  10326  elfz2nn0  10347  elfzo2  10385  elfzo3  10399  lbfzo0  10420  fzind2  10486  zmodid2  10615  swrdccatin1  11307  swrdccat  11317  redivap  11436  imdivap  11443  maxleast  11775  cosmul  12308  bitsval  12506  bitsmod  12519  bitscmp  12521  dfgcd2  12587  lcmneg  12648  coprmgcdb  12662  divgcdcoprmex  12676  cncongr1  12677  cncongr2  12678  difsqpwdvds  12913  elgz  12946  xpsfrnel  13429  xpsfrnel2  13431  mgmsscl  13446  ismhm  13546  mhmpropd  13551  issubm  13557  issubg  13762  eqglact  13814  eqgid  13815  ecqusaddd  13827  ecqusaddcl  13828  isrng  13950  issrg  13981  srglmhm  14009  srgrmhm  14010  isring  14016  ringlghm  14077  dfrhm2  14171  issubrng  14216  issubrg3  14264  islmod  14308  islssm  14374  islssmg  14375  lsspropdg  14448  qusmulrng  14549  lmbrf  14942  uptx  15001  txcn  15002  xmetec  15164  bl2ioo  15277  lgsmodeq  15777  lgsmulsqcoprm  15778  uspgredg2v  16075  wksfval  16176  wlkeq  16208  isclwwlk  16248  clwwlkbp  16249  isclwwlknx  16270  clwwlknp  16271  clwwlkn1  16272  clwwlkn2  16275  clwwlknonel  16286  findset  16561