Theorem 3anass 1009

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 1007	. 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 1005

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 1007

This theorem is referenced by:  3anrot  1010  3anan12  1017  anandi3  1018  3biant1d  1392  3exdistr  1967  r3al  2588  ceqsex2  2857  ceqsex3v  2859  ceqsex4v  2860  ceqsex6v  2861  ceqsex8v  2862  eldifpr  3721  rexdifpr  3722  trel3  4221  sowlin  4446  dff1o4  5627  mpoxopovel  6485  dfsmo2  6531  ecopovtrn  6879  ecopovtrng  6882  elixp2  6950  elixp  6953  mptelixpg  6982  eqinfti  7324  distrnqg  7718  recmulnqg  7722  ltexnqq  7739  enq0tr  7765  distrnq0  7790  genpdflem  7838  distrlem1prl  7913  distrlem1pru  7914  divmulasscomap  8990  muldivdirap  9001  divmuldivap  9006  prime  9698  eluz2  9880  raluz2  9932  elixx1  10252  elixx3g  10256  elioo2  10276  elioo5  10288  elicc4  10295  iccneg  10344  icoshft  10345  elfz1  10369  elfz  10370  elfz2  10371  elfzm11  10450  elfz2nn0  10471  elfzo2  10509  elfzo3  10523  lbfzo0  10544  fzind2  10610  zmodid2  10741  swrdccatin1  11445  swrdccat  11455  redivap  11587  imdivap  11594  maxleast  11926  cosmul  12459  bitsval  12657  bitsmod  12670  bitscmp  12672  dfgcd2  12738  lcmneg  12799  coprmgcdb  12813  divgcdcoprmex  12827  cncongr1  12828  cncongr2  12829  difsqpwdvds  13064  elgz  13097  xpsfrnel  13611  xpsfrnel2  13613  mgmsscl  13627  ismhm  13719  mhmpropd  13724  issubm  13730  issubg  13929  eqglact  13981  eqgid  13982  ecqusaddd  13994  ecqusaddcl  13995  isrng  14176  issrg  14211  srglmhm  14239  srgrmhm  14240  isring  14246  ringlghm  14307  dfrhm2  14402  issubrng  14448  issubrg3  14496  islmod  14568  islssm  14634  islssmg  14635  lsspropdg  14708  qusmulrng  14809  lmbrf  15209  uptx  15268  txcn  15269  xmetec  15431  bl2ioo  15544  lgsmodeq  16047  lgsmulsqcoprm  16048  uspgredg2v  16345  wksfval  16446  wlkeq  16478  isclwwlk  16518  clwwlkbp  16519  isclwwlknx  16540  clwwlknp  16541  clwwlkn1  16542  clwwlkn2  16545  clwwlknonel  16556  findset  16854