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  1964  r3al  2577  ceqsex2  2845  ceqsex3v  2847  ceqsex4v  2848  ceqsex6v  2849  ceqsex8v  2850  eldifpr  3700  rexdifpr  3701  trel3  4200  sowlin  4423  dff1o4  5600  mpoxopovel  6450  dfsmo2  6496  ecopovtrn  6844  ecopovtrng  6847  elixp2  6914  elixp  6917  mptelixpg  6946  eqinfti  7262  distrnqg  7650  recmulnqg  7654  ltexnqq  7671  enq0tr  7697  distrnq0  7722  genpdflem  7770  distrlem1prl  7845  distrlem1pru  7846  divmulasscomap  8919  muldivdirap  8930  divmuldivap  8935  prime  9622  eluz2  9804  raluz2  9856  elixx1  10175  elixx3g  10179  elioo2  10199  elioo5  10211  elicc4  10218  iccneg  10267  icoshft  10268  elfz1  10291  elfz  10292  elfz2  10293  elfzm11  10369  elfz2nn0  10390  elfzo2  10428  elfzo3  10442  lbfzo0  10463  fzind2  10529  zmodid2  10658  swrdccatin1  11353  swrdccat  11363  redivap  11495  imdivap  11502  maxleast  11834  cosmul  12367  bitsval  12565  bitsmod  12578  bitscmp  12580  dfgcd2  12646  lcmneg  12707  coprmgcdb  12721  divgcdcoprmex  12735  cncongr1  12736  cncongr2  12737  difsqpwdvds  12972  elgz  13005  xpsfrnel  13488  xpsfrnel2  13490  mgmsscl  13505  ismhm  13605  mhmpropd  13610  issubm  13616  issubg  13821  eqglact  13873  eqgid  13874  ecqusaddd  13886  ecqusaddcl  13887  isrng  14009  issrg  14040  srglmhm  14068  srgrmhm  14069  isring  14075  ringlghm  14136  dfrhm2  14230  issubrng  14275  issubrg3  14323  islmod  14367  islssm  14433  islssmg  14434  lsspropdg  14507  qusmulrng  14608  lmbrf  15006  uptx  15065  txcn  15066  xmetec  15228  bl2ioo  15341  lgsmodeq  15844  lgsmulsqcoprm  15845  uspgredg2v  16142  wksfval  16243  wlkeq  16275  isclwwlk  16315  clwwlkbp  16316  isclwwlknx  16337  clwwlknp  16338  clwwlkn1  16339  clwwlkn2  16342  clwwlknonel  16353  findset  16641