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  1965  r3al  2586  ceqsex2  2854  ceqsex3v  2856  ceqsex4v  2857  ceqsex6v  2858  ceqsex8v  2859  eldifpr  3715  rexdifpr  3716  trel3  4215  sowlin  4440  dff1o4  5621  mpoxopovel  6471  dfsmo2  6517  ecopovtrn  6865  ecopovtrng  6868  elixp2  6936  elixp  6939  mptelixpg  6968  eqinfti  7310  distrnqg  7698  recmulnqg  7702  ltexnqq  7719  enq0tr  7745  distrnq0  7770  genpdflem  7818  distrlem1prl  7893  distrlem1pru  7894  divmulasscomap  8966  muldivdirap  8977  divmuldivap  8982  prime  9673  eluz2  9855  raluz2  9907  elixx1  10226  elixx3g  10230  elioo2  10250  elioo5  10262  elicc4  10269  iccneg  10318  icoshft  10319  elfz1  10343  elfz  10344  elfz2  10345  elfzm11  10421  elfz2nn0  10442  elfzo2  10480  elfzo3  10494  lbfzo0  10515  fzind2  10581  zmodid2  10710  swrdccatin1  11410  swrdccat  11420  redivap  11552  imdivap  11559  maxleast  11891  cosmul  12424  bitsval  12622  bitsmod  12635  bitscmp  12637  dfgcd2  12703  lcmneg  12764  coprmgcdb  12778  divgcdcoprmex  12792  cncongr1  12793  cncongr2  12794  difsqpwdvds  13029  elgz  13062  xpsfrnel  13546  xpsfrnel2  13548  mgmsscl  13563  ismhm  13663  mhmpropd  13668  issubm  13674  issubg  13879  eqglact  13931  eqgid  13932  ecqusaddd  13944  ecqusaddcl  13945  isrng  14067  issrg  14098  srglmhm  14126  srgrmhm  14127  isring  14133  ringlghm  14194  dfrhm2  14288  issubrng  14333  issubrg3  14381  islmod  14426  islssm  14492  islssmg  14493  lsspropdg  14566  qusmulrng  14667  lmbrf  15067  uptx  15126  txcn  15127  xmetec  15289  bl2ioo  15402  lgsmodeq  15905  lgsmulsqcoprm  15906  uspgredg2v  16203  wksfval  16304  wlkeq  16336  isclwwlk  16376  clwwlkbp  16377  isclwwlknx  16398  clwwlknp  16399  clwwlkn1  16400  clwwlkn2  16403  clwwlknonel  16414  findset  16702