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  4237  sowlin  4465  dff1o4  5647  mpoxopovel  6512  dfsmo2  6558  ecopovtrn  6906  ecopovtrng  6909  elixp2  6984  elixp  6987  mptelixpg  7016  eqinfti  7360  distrnqg  7754  recmulnqg  7758  ltexnqq  7775  enq0tr  7801  distrnq0  7826  genpdflem  7874  distrlem1prl  7949  distrlem1pru  7950  divmulasscomap  9027  muldivdirap  9038  divmuldivap  9043  prime  9747  eluz2  9929  raluz2  9981  elixx1  10301  elixx3g  10305  elioo2  10325  elioo5  10337  elicc4  10344  iccneg  10393  icoshft  10394  elfz1  10418  elfz  10419  elfz2  10420  elfzm11  10500  elfz2nn0  10521  elfzo2  10559  elfzo3  10573  lbfzo0  10594  fzind2  10660  zmodid2  10791  swrdccatin1  11499  swrdccat  11509  redivap  11641  imdivap  11648  maxleast  11981  cosmul  12514  bitsval  12712  bitsmod  12725  bitscmp  12727  dfgcd2  12793  lcmneg  12854  coprmgcdb  12868  divgcdcoprmex  12882  cncongr1  12883  cncongr2  12884  difsqpwdvds  13119  elgz  13152  xpsfrnel  13667  xpsfrnel2  13669  mgmsscl  13683  ismhm  13770  mhmpropd  13775  issubm  13781  issubg  13978  eqglact  14030  eqgid  14031  ecqusaddd  14043  ecqusaddcl  14044  isrng  14235  issrg  14271  srglmhm  14299  srgrmhm  14300  isring  14306  ringlghm  14368  dfrhm2  14463  issubrng  14509  issubrg3  14557  islmod  14629  islssm  14696  islssmg  14697  lsspropdg  14770  qusmulrng  14871  lmbrf  15318  uptx  15377  txcn  15378  xmetec  15540  bl2ioo  15653  lgsmodeq  16176  lgsmulsqcoprm  16177  uspgredg2v  16474  wksfval  16575  wlkeq  16607  isclwwlk  16647  clwwlkbp  16648  isclwwlknx  16669  clwwlknp  16670  clwwlkn1  16671  clwwlkn2  16674  clwwlknonel  16685  findset  16983