Theorem 3anass 1006

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

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 1004

This theorem is referenced by:  3anrot  1007  3anan12  1014  anandi3  1015  3biant1d  1389  3exdistr  1962  r3al  2574  ceqsex2  2841  ceqsex3v  2843  ceqsex4v  2844  ceqsex6v  2845  ceqsex8v  2846  eldifpr  3693  rexdifpr  3694  trel3  4190  sowlin  4412  dff1o4  5585  mpoxopovel  6398  dfsmo2  6444  ecopovtrn  6792  ecopovtrng  6795  elixp2  6862  elixp  6865  mptelixpg  6894  eqinfti  7203  distrnqg  7590  recmulnqg  7594  ltexnqq  7611  enq0tr  7637  distrnq0  7662  genpdflem  7710  distrlem1prl  7785  distrlem1pru  7786  divmulasscomap  8859  muldivdirap  8870  divmuldivap  8875  prime  9562  eluz2  9744  raluz2  9791  elixx1  10110  elixx3g  10114  elioo2  10134  elioo5  10146  elicc4  10153  iccneg  10202  icoshft  10203  elfz1  10226  elfz  10227  elfz2  10228  elfzm11  10304  elfz2nn0  10325  elfzo2  10363  elfzo3  10377  lbfzo0  10398  fzind2  10462  zmodid2  10591  swrdccatin1  11278  swrdccat  11288  redivap  11406  imdivap  11413  maxleast  11745  cosmul  12277  bitsval  12475  bitsmod  12488  bitscmp  12490  dfgcd2  12556  lcmneg  12617  coprmgcdb  12631  divgcdcoprmex  12645  cncongr1  12646  cncongr2  12647  difsqpwdvds  12882  elgz  12915  xpsfrnel  13398  xpsfrnel2  13400  mgmsscl  13415  ismhm  13515  mhmpropd  13520  issubm  13526  issubg  13731  eqglact  13783  eqgid  13784  ecqusaddd  13796  ecqusaddcl  13797  isrng  13918  issrg  13949  srglmhm  13977  srgrmhm  13978  isring  13984  ringlghm  14045  dfrhm2  14139  issubrng  14184  issubrg3  14232  islmod  14276  islssm  14342  islssmg  14343  lsspropdg  14416  qusmulrng  14517  lmbrf  14910  uptx  14969  txcn  14970  xmetec  15132  bl2ioo  15245  lgsmodeq  15745  lgsmulsqcoprm  15746  uspgredg2v  16040  wksfval  16094  wlkeq  16126  isclwwlk  16163  clwwlkbp  16164  isclwwlknx  16184  clwwlknp  16185  clwwlkn1  16186  clwwlkn2  16189  findset  16417