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  3718  rexdifpr  3719  trel3  4218  sowlin  4443  dff1o4  5624  mpoxopovel  6474  dfsmo2  6520  ecopovtrn  6868  ecopovtrng  6871  elixp2  6939  elixp  6942  mptelixpg  6971  eqinfti  7313  distrnqg  7707  recmulnqg  7711  ltexnqq  7728  enq0tr  7754  distrnq0  7779  genpdflem  7827  distrlem1prl  7902  distrlem1pru  7903  divmulasscomap  8975  muldivdirap  8986  divmuldivap  8991  prime  9683  eluz2  9865  raluz2  9917  elixx1  10236  elixx3g  10240  elioo2  10260  elioo5  10272  elicc4  10279  iccneg  10328  icoshft  10329  elfz1  10353  elfz  10354  elfz2  10355  elfzm11  10432  elfz2nn0  10453  elfzo2  10491  elfzo3  10505  lbfzo0  10526  fzind2  10592  zmodid2  10721  swrdccatin1  11425  swrdccat  11435  redivap  11567  imdivap  11574  maxleast  11906  cosmul  12439  bitsval  12637  bitsmod  12650  bitscmp  12652  dfgcd2  12718  lcmneg  12779  coprmgcdb  12793  divgcdcoprmex  12807  cncongr1  12808  cncongr2  12809  difsqpwdvds  13044  elgz  13077  xpsfrnel  13578  xpsfrnel2  13580  mgmsscl  13595  ismhm  13695  mhmpropd  13700  issubm  13706  issubg  13911  eqglact  13963  eqgid  13964  ecqusaddd  13976  ecqusaddcl  13977  isrng  14099  issrg  14130  srglmhm  14158  srgrmhm  14159  isring  14165  ringlghm  14226  dfrhm2  14321  issubrng  14367  issubrg3  14415  islmod  14488  islssm  14554  islssmg  14555  lsspropdg  14628  qusmulrng  14729  lmbrf  15129  uptx  15188  txcn  15189  xmetec  15351  bl2ioo  15464  lgsmodeq  15967  lgsmulsqcoprm  15968  uspgredg2v  16265  wksfval  16366  wlkeq  16398  isclwwlk  16438  clwwlkbp  16439  isclwwlknx  16460  clwwlknp  16461  clwwlkn1  16462  clwwlkn2  16465  clwwlknonel  16476  findset  16764