Theorem 3anass 1008

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

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 1006

This theorem is referenced by:  3anrot  1009  3anan12  1016  anandi3  1017  3biant1d  1391  3exdistr  1963  r3al  2575  ceqsex2  2843  ceqsex3v  2845  ceqsex4v  2846  ceqsex6v  2847  ceqsex8v  2848  eldifpr  3697  rexdifpr  3698  trel3  4196  sowlin  4419  dff1o4  5594  mpoxopovel  6412  dfsmo2  6458  ecopovtrn  6806  ecopovtrng  6809  elixp2  6876  elixp  6879  mptelixpg  6908  eqinfti  7224  distrnqg  7612  recmulnqg  7616  ltexnqq  7633  enq0tr  7659  distrnq0  7684  genpdflem  7732  distrlem1prl  7807  distrlem1pru  7808  divmulasscomap  8881  muldivdirap  8892  divmuldivap  8897  prime  9584  eluz2  9766  raluz2  9818  elixx1  10137  elixx3g  10141  elioo2  10161  elioo5  10173  elicc4  10180  iccneg  10229  icoshft  10230  elfz1  10253  elfz  10254  elfz2  10255  elfzm11  10331  elfz2nn0  10352  elfzo2  10390  elfzo3  10404  lbfzo0  10425  fzind2  10491  zmodid2  10620  swrdccatin1  11315  swrdccat  11325  redivap  11457  imdivap  11464  maxleast  11796  cosmul  12329  bitsval  12527  bitsmod  12540  bitscmp  12542  dfgcd2  12608  lcmneg  12669  coprmgcdb  12683  divgcdcoprmex  12697  cncongr1  12698  cncongr2  12699  difsqpwdvds  12934  elgz  12967  xpsfrnel  13450  xpsfrnel2  13452  mgmsscl  13467  ismhm  13567  mhmpropd  13572  issubm  13578  issubg  13783  eqglact  13835  eqgid  13836  ecqusaddd  13848  ecqusaddcl  13849  isrng  13971  issrg  14002  srglmhm  14030  srgrmhm  14031  isring  14037  ringlghm  14098  dfrhm2  14192  issubrng  14237  issubrg3  14285  islmod  14329  islssm  14395  islssmg  14396  lsspropdg  14469  qusmulrng  14570  lmbrf  14968  uptx  15027  txcn  15028  xmetec  15190  bl2ioo  15303  lgsmodeq  15803  lgsmulsqcoprm  15804  uspgredg2v  16101  wksfval  16202  wlkeq  16234  isclwwlk  16274  clwwlkbp  16275  isclwwlknx  16296  clwwlknp  16297  clwwlkn1  16298  clwwlkn2  16301  clwwlknonel  16312  findset  16600