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 ) ) )

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 1009

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 1011

This theorem is referenced by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3735  rexdifpr  3736  trel3  4235  sowlin  4463  dff1o4  5645  mpoxopovel  6506  dfsmo2  6552  ecopovtrn  6900  ecopovtrng  6903  elixp2  6978  elixp  6981  mptelixpg  7010  eqinfti  7354  distrnqg  7748  recmulnqg  7752  ltexnqq  7769  enq0tr  7795  distrnq0  7820  genpdflem  7868  distrlem1prl  7943  distrlem1pru  7944  divmulasscomap  9020  muldivdirap  9031  divmuldivap  9036  prime  9728  eluz2  9910  raluz2  9962  elixx1  10282  elixx3g  10286  elioo2  10306  elioo5  10318  elicc4  10325  iccneg  10374  icoshft  10375  elfz1  10399  elfz  10400  elfz2  10401  elfzm11  10481  elfz2nn0  10502  elfzo2  10540  elfzo3  10554  lbfzo0  10575  fzind2  10641  zmodid2  10772  swrdccatin1  11480  swrdccat  11490  redivap  11622  imdivap  11629  maxleast  11962  cosmul  12495  bitsval  12693  bitsmod  12706  bitscmp  12708  dfgcd2  12774  lcmneg  12835  coprmgcdb  12849  divgcdcoprmex  12863  cncongr1  12864  cncongr2  12865  difsqpwdvds  13100  elgz  13133  xpsfrnel  13648  xpsfrnel2  13650  mgmsscl  13664  ismhm  13751  mhmpropd  13756  issubm  13762  issubg  13959  eqglact  14011  eqgid  14012  ecqusaddd  14024  ecqusaddcl  14025  isrng  14216  issrg  14252  srglmhm  14280  srgrmhm  14281  isring  14287  ringlghm  14349  dfrhm2  14444  issubrng  14490  issubrg3  14538  islmod  14610  islssm  14677  islssmg  14678  lsspropdg  14751  qusmulrng  14852  lmbrf  15299  uptx  15358  txcn  15359  xmetec  15521  bl2ioo  15634  lgsmodeq  16147  lgsmulsqcoprm  16148  uspgredg2v  16445  wksfval  16546  wlkeq  16578  isclwwlk  16618  clwwlkbp  16619  isclwwlknx  16640  clwwlknp  16641  clwwlkn1  16642  clwwlkn2  16645  clwwlknonel  16656  findset  16954