Theorem 3anass 1013

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3736  rexdifpr  3737  trel3  4239  sowlin  4467  dff1o4  5650  mpoxopovel  6517  dfsmo2  6563  ecopovtrn  6911  ecopovtrng  6914  elixp2  6990  elixp  6993  mptelixpg  7022  eqinfti  7367  distrnqg  7761  recmulnqg  7765  ltexnqq  7782  enq0tr  7808  distrnq0  7833  genpdflem  7881  distrlem1prl  7956  distrlem1pru  7957  divmulasscomap  9035  muldivdirap  9046  divmuldivap  9051  prime  9756  eluz2  9943  raluz2  9995  elixx1  10316  elixx3g  10320  elioo2  10340  elioo5  10352  elicc4  10359  iccneg  10408  icoshft  10409  elfz1  10433  elfz  10434  elfz2  10435  elfzm11  10515  elfz2nn0  10536  elfzo2  10574  elfzo3  10588  lbfzo0  10609  fzind2  10675  zmodid2  10810  swrdccatin1  11519  swrdccat  11529  redivap  11661  imdivap  11668  maxleast  12002  cosmul  12537  bitsval  12735  bitsmod  12748  bitscmp  12750  dfgcd2  12816  lcmneg  12877  coprmgcdb  12891  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  difsqpwdvds  13146  elgz  13179  xpsfrnel  13724  xpsfrnel2  13726  mgmsscl  13740  ismhm  13827  mhmpropd  13832  issubm  13838  issubg  14035  eqglact  14087  eqgid  14088  ecqusaddd  14100  ecqusaddcl  14101  isrng  14340  issrg  14376  srglmhm  14404  srgrmhm  14405  isring  14411  ringlghm  14473  dfrhm2  14570  issubrng  14616  issubrg3  14664  islmod  14736  islssm  14803  islssmg  14804  lsspropdg  14877  qusmulrng  14978  lmbrf  15474  uptx  15533  txcn  15534  xmetec  15696  bl2ioo  15809  lgsmodeq  16402  lgsmulsqcoprm  16403  uspgredg2v  16700  wksfval  16801  wlkeq  16833  isclwwlk  16873  clwwlkbp  16874  isclwwlknx  16895  clwwlknp  16896  clwwlkn1  16897  clwwlkn2  16900  clwwlknonel  16911  findset  17209