Theorem 3anass 984

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

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 982

This theorem is referenced by:  3anrot  985  3anan12  992  anandi3  993  3exdistr  1930  r3al  2541  ceqsex2  2804  ceqsex3v  2806  ceqsex4v  2807  ceqsex6v  2808  ceqsex8v  2809  eldifpr  3650  rexdifpr  3651  trel3  4140  sowlin  4356  dff1o4  5515  mpoxopovel  6308  dfsmo2  6354  ecopovtrn  6700  ecopovtrng  6703  elixp2  6770  elixp  6773  mptelixpg  6802  eqinfti  7095  distrnqg  7473  recmulnqg  7477  ltexnqq  7494  enq0tr  7520  distrnq0  7545  genpdflem  7593  distrlem1prl  7668  distrlem1pru  7669  divmulasscomap  8742  muldivdirap  8753  divmuldivap  8758  prime  9444  eluz2  9626  raluz2  9672  elixx1  9991  elixx3g  9995  elioo2  10015  elioo5  10027  elicc4  10034  iccneg  10083  icoshft  10084  elfz1  10107  elfz  10108  elfz2  10109  elfzm11  10185  elfz2nn0  10206  elfzo2  10244  elfzo3  10258  lbfzo0  10276  fzind2  10334  zmodid2  10463  redivap  11058  imdivap  11065  maxleast  11397  cosmul  11929  bitsval  12127  bitsmod  12140  bitscmp  12142  dfgcd2  12208  lcmneg  12269  coprmgcdb  12283  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  difsqpwdvds  12534  elgz  12567  xpsfrnel  13048  xpsfrnel2  13050  mgmsscl  13065  ismhm  13165  mhmpropd  13170  issubm  13176  issubg  13381  eqglact  13433  eqgid  13434  ecqusaddd  13446  ecqusaddcl  13447  isrng  13568  issrg  13599  srglmhm  13627  srgrmhm  13628  isring  13634  ringlghm  13695  dfrhm2  13788  issubrng  13833  issubrg3  13881  islmod  13925  islssm  13991  islssmg  13992  lsspropdg  14065  qusmulrng  14166  lmbrf  14559  uptx  14618  txcn  14619  xmetec  14781  bl2ioo  14894  lgsmodeq  15394  lgsmulsqcoprm  15395  findset  15699