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  1927  r3al  2534  ceqsex2  2792  ceqsex3v  2794  ceqsex4v  2795  ceqsex6v  2796  ceqsex8v  2797  eldifpr  3634  rexdifpr  3635  trel3  4124  sowlin  4338  dff1o4  5488  mpoxopovel  6267  dfsmo2  6313  ecopovtrn  6659  ecopovtrng  6662  elixp2  6729  elixp  6732  mptelixpg  6761  eqinfti  7050  distrnqg  7417  recmulnqg  7421  ltexnqq  7438  enq0tr  7464  distrnq0  7489  genpdflem  7537  distrlem1prl  7612  distrlem1pru  7613  divmulasscomap  8684  muldivdirap  8695  divmuldivap  8700  prime  9383  eluz2  9565  raluz2  9611  elixx1  9929  elixx3g  9933  elioo2  9953  elioo5  9965  elicc4  9972  iccneg  10021  icoshft  10022  elfz1  10045  elfz  10046  elfz2  10047  elfzm11  10123  elfz2nn0  10144  elfzo2  10182  elfzo3  10195  lbfzo0  10213  fzind2  10271  zmodid2  10385  redivap  10918  imdivap  10925  maxleast  11257  cosmul  11788  dfgcd2  12050  lcmneg  12109  coprmgcdb  12123  divgcdcoprmex  12137  cncongr1  12138  cncongr2  12139  difsqpwdvds  12373  elgz  12406  xpsfrnel  12823  xpsfrnel2  12825  mgmsscl  12840  ismhm  12928  mhmpropd  12933  issubm  12939  issubg  13129  eqglact  13181  eqgid  13182  ecqusaddd  13194  ecqusaddcl  13195  isrng  13305  issrg  13336  srglmhm  13364  srgrmhm  13365  isring  13371  dfrhm2  13521  issubrng  13563  issubrg3  13611  islmod  13624  islssm  13690  islssmg  13691  lsspropdg  13764  qusmulrng  13863  lmbrf  14192  uptx  14251  txcn  14252  xmetec  14414  bl2ioo  14519  lgsmodeq  14924  lgsmulsqcoprm  14925  findset  15175