Theorem 3anass 982

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 980	. 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 978

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 980

This theorem is referenced by:  3anrot  983  3anan12  990  anandi3  991  3exdistr  1915  r3al  2521  ceqsex2  2779  ceqsex3v  2781  ceqsex4v  2782  ceqsex6v  2783  ceqsex8v  2784  eldifpr  3621  rexdifpr  3622  trel3  4111  sowlin  4322  dff1o4  5471  mpoxopovel  6244  dfsmo2  6290  ecopovtrn  6634  ecopovtrng  6637  elixp2  6704  elixp  6707  mptelixpg  6736  eqinfti  7021  distrnqg  7388  recmulnqg  7392  ltexnqq  7409  enq0tr  7435  distrnq0  7460  genpdflem  7508  distrlem1prl  7583  distrlem1pru  7584  divmulasscomap  8655  muldivdirap  8666  divmuldivap  8671  prime  9354  eluz2  9536  raluz2  9581  elixx1  9899  elixx3g  9903  elioo2  9923  elioo5  9935  elicc4  9942  iccneg  9991  icoshft  9992  elfz1  10015  elfz  10016  elfz2  10017  elfzm11  10093  elfz2nn0  10114  elfzo2  10152  elfzo3  10165  lbfzo0  10183  fzind2  10241  zmodid2  10354  redivap  10885  imdivap  10892  maxleast  11224  cosmul  11755  dfgcd2  12017  lcmneg  12076  coprmgcdb  12090  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  difsqpwdvds  12339  elgz  12371  xpsfrnel  12768  xpsfrnel2  12770  mgmsscl  12785  ismhm  12858  mhmpropd  12862  issubm  12868  issubg  13038  eqglact  13089  eqgid  13090  issrg  13153  srglmhm  13181  srgrmhm  13182  isring  13188  issubrg3  13373  islmod  13386  islssm  13450  lmbrf  13754  uptx  13813  txcn  13814  xmetec  13976  bl2ioo  14081  lgsmodeq  14485  lgsmulsqcoprm  14486  findset  14736