Theorem 3anass 1006

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 1004	. 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 1002

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 1004

This theorem is referenced by:  3anrot  1007  3anan12  1014  anandi3  1015  3biant1d  1389  3exdistr  1962  r3al  2574  ceqsex2  2842  ceqsex3v  2844  ceqsex4v  2845  ceqsex6v  2846  ceqsex8v  2847  eldifpr  3694  rexdifpr  3695  trel3  4193  sowlin  4415  dff1o4  5588  mpoxopovel  6402  dfsmo2  6448  ecopovtrn  6796  ecopovtrng  6799  elixp2  6866  elixp  6869  mptelixpg  6898  eqinfti  7213  distrnqg  7600  recmulnqg  7604  ltexnqq  7621  enq0tr  7647  distrnq0  7672  genpdflem  7720  distrlem1prl  7795  distrlem1pru  7796  divmulasscomap  8869  muldivdirap  8880  divmuldivap  8885  prime  9572  eluz2  9754  raluz2  9806  elixx1  10125  elixx3g  10129  elioo2  10149  elioo5  10161  elicc4  10168  iccneg  10217  icoshft  10218  elfz1  10241  elfz  10242  elfz2  10243  elfzm11  10319  elfz2nn0  10340  elfzo2  10378  elfzo3  10392  lbfzo0  10413  fzind2  10478  zmodid2  10607  swrdccatin1  11299  swrdccat  11309  redivap  11428  imdivap  11435  maxleast  11767  cosmul  12299  bitsval  12497  bitsmod  12510  bitscmp  12512  dfgcd2  12578  lcmneg  12639  coprmgcdb  12653  divgcdcoprmex  12667  cncongr1  12668  cncongr2  12669  difsqpwdvds  12904  elgz  12937  xpsfrnel  13420  xpsfrnel2  13422  mgmsscl  13437  ismhm  13537  mhmpropd  13542  issubm  13548  issubg  13753  eqglact  13805  eqgid  13806  ecqusaddd  13818  ecqusaddcl  13819  isrng  13940  issrg  13971  srglmhm  13999  srgrmhm  14000  isring  14006  ringlghm  14067  dfrhm2  14161  issubrng  14206  issubrg3  14254  islmod  14298  islssm  14364  islssmg  14365  lsspropdg  14438  qusmulrng  14539  lmbrf  14932  uptx  14991  txcn  14992  xmetec  15154  bl2ioo  15267  lgsmodeq  15767  lgsmulsqcoprm  15768  uspgredg2v  16065  wksfval  16133  wlkeq  16165  isclwwlk  16203  clwwlkbp  16204  isclwwlknx  16225  clwwlknp  16226  clwwlkn1  16227  clwwlkn2  16230  clwwlknonel  16241  findset  16490