Theorem 3anass 978

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 976	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 399	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 183	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 103   <-> wb 104   /\ w3a 974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 976

This theorem is referenced by:  3anrot  979  3anan12  986  anandi3  987  3exdistr  1909  r3al  2515  ceqsex2  2771  ceqsex3v  2773  ceqsex4v  2774  ceqsex6v  2775  ceqsex8v  2776  eldifpr  3611  rexdifpr  3612  trel3  4096  sowlin  4306  dff1o4  5453  mpoxopovel  6224  dfsmo2  6270  ecopovtrn  6614  ecopovtrng  6617  elixp2  6684  elixp  6687  mptelixpg  6716  eqinfti  7001  distrnqg  7353  recmulnqg  7357  ltexnqq  7374  enq0tr  7400  distrnq0  7425  genpdflem  7473  distrlem1prl  7548  distrlem1pru  7549  divmulasscomap  8617  muldivdirap  8628  divmuldivap  8633  prime  9315  eluz2  9497  raluz2  9542  elixx1  9858  elixx3g  9862  elioo2  9882  elioo5  9894  elicc4  9901  iccneg  9950  icoshft  9951  elfz1  9974  elfz  9975  elfz2  9976  elfzm11  10051  elfz2nn0  10072  elfzo2  10110  elfzo3  10123  lbfzo0  10141  fzind2  10199  zmodid2  10312  redivap  10842  imdivap  10849  maxleast  11181  cosmul  11712  dfgcd2  11973  lcmneg  12032  coprmgcdb  12046  divgcdcoprmex  12060  cncongr1  12061  cncongr2  12062  difsqpwdvds  12295  elgz  12327  mgmsscl  12619  ismhm  12689  mhmpropd  12693  issubm  12699  lmbrf  13094  uptx  13153  txcn  13154  xmetec  13316  bl2ioo  13421  lgsmodeq  13825  lgsmulsqcoprm  13826  findset  14065