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  4411  dff1o4  5582  mpoxopovel  6393  dfsmo2  6439  ecopovtrn  6787  ecopovtrng  6790  elixp2  6857  elixp  6860  mptelixpg  6889  eqinfti  7195  distrnqg  7582  recmulnqg  7586  ltexnqq  7603  enq0tr  7629  distrnq0  7654  genpdflem  7702  distrlem1prl  7777  distrlem1pru  7778  divmulasscomap  8851  muldivdirap  8862  divmuldivap  8867  prime  9554  eluz2  9736  raluz2  9782  elixx1  10101  elixx3g  10105  elioo2  10125  elioo5  10137  elicc4  10144  iccneg  10193  icoshft  10194  elfz1  10217  elfz  10218  elfz2  10219  elfzm11  10295  elfz2nn0  10316  elfzo2  10354  elfzo3  10368  lbfzo0  10389  fzind2  10453  zmodid2  10582  swrdccatin1  11265  swrdccat  11275  redivap  11393  imdivap  11400  maxleast  11732  cosmul  12264  bitsval  12462  bitsmod  12475  bitscmp  12477  dfgcd2  12543  lcmneg  12604  coprmgcdb  12618  divgcdcoprmex  12632  cncongr1  12633  cncongr2  12634  difsqpwdvds  12869  elgz  12902  xpsfrnel  13385  xpsfrnel2  13387  mgmsscl  13402  ismhm  13502  mhmpropd  13507  issubm  13513  issubg  13718  eqglact  13770  eqgid  13771  ecqusaddd  13783  ecqusaddcl  13784  isrng  13905  issrg  13936  srglmhm  13964  srgrmhm  13965  isring  13971  ringlghm  14032  dfrhm2  14126  issubrng  14171  issubrg3  14219  islmod  14263  islssm  14329  islssmg  14330  lsspropdg  14403  qusmulrng  14504  lmbrf  14897  uptx  14956  txcn  14957  xmetec  15119  bl2ioo  15232  lgsmodeq  15732  lgsmulsqcoprm  15733  uspgredg2v  16027  wksfval  16043  wlkeq  16075  findset  16332