Theorem 3anass 1013

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 1011	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 405	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 184	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3736  rexdifpr  3737  trel3  4237  sowlin  4465  dff1o4  5647  mpoxopovel  6512  dfsmo2  6558  ecopovtrn  6906  ecopovtrng  6909  elixp2  6984  elixp  6987  mptelixpg  7016  eqinfti  7361  distrnqg  7755  recmulnqg  7759  ltexnqq  7776  enq0tr  7802  distrnq0  7827  genpdflem  7875  distrlem1prl  7950  distrlem1pru  7951  divmulasscomap  9029  muldivdirap  9040  divmuldivap  9045  prime  9750  eluz2  9937  raluz2  9989  elixx1  10310  elixx3g  10314  elioo2  10334  elioo5  10346  elicc4  10353  iccneg  10402  icoshft  10403  elfz1  10427  elfz  10428  elfz2  10429  elfzm11  10509  elfz2nn0  10530  elfzo2  10568  elfzo3  10582  lbfzo0  10603  fzind2  10669  zmodid2  10803  swrdccatin1  11512  swrdccat  11522  redivap  11654  imdivap  11661  maxleast  11995  cosmul  12530  bitsval  12728  bitsmod  12741  bitscmp  12743  dfgcd2  12809  lcmneg  12870  coprmgcdb  12884  divgcdcoprmex  12898  cncongr1  12899  cncongr2  12900  difsqpwdvds  13139  elgz  13172  xpsfrnel  13716  xpsfrnel2  13718  mgmsscl  13732  ismhm  13819  mhmpropd  13824  issubm  13830  issubg  14027  eqglact  14079  eqgid  14080  ecqusaddd  14092  ecqusaddcl  14093  isrng  14284  issrg  14320  srglmhm  14348  srgrmhm  14349  isring  14355  ringlghm  14417  dfrhm2  14512  issubrng  14558  issubrg3  14606  islmod  14678  islssm  14745  islssmg  14746  lsspropdg  14819  qusmulrng  14920  lmbrf  15368  uptx  15427  txcn  15428  xmetec  15590  bl2ioo  15703  lgsmodeq  16286  lgsmulsqcoprm  16287  uspgredg2v  16584  wksfval  16685  wlkeq  16717  isclwwlk  16757  clwwlkbp  16758  isclwwlknx  16779  clwwlknp  16780  clwwlkn1  16781  clwwlkn2  16784  clwwlknonel  16795  findset  17093