Theorem 3anass 966

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 964	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 398	. 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 962

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 964

This theorem is referenced by:  3anrot  967  3anan12  974  anandi3  975  3exdistr  1887  r3al  2475  ceqsex2  2721  ceqsex3v  2723  ceqsex4v  2724  ceqsex6v  2725  ceqsex8v  2726  trel3  4029  sowlin  4237  dff1o4  5368  mpoxopovel  6131  dfsmo2  6177  ecopovtrn  6519  ecopovtrng  6522  elixp2  6589  elixp  6592  mptelixpg  6621  eqinfti  6900  distrnqg  7188  recmulnqg  7192  ltexnqq  7209  enq0tr  7235  distrnq0  7260  genpdflem  7308  distrlem1prl  7383  distrlem1pru  7384  divmulasscomap  8449  muldivdirap  8460  divmuldivap  8465  prime  9143  eluz2  9325  raluz2  9367  elixx1  9673  elixx3g  9677  elioo2  9697  elioo5  9709  elicc4  9716  iccneg  9765  icoshft  9766  elfz1  9788  elfz  9789  elfz2  9790  elfzm11  9864  elfz2nn0  9885  elfzo2  9920  elfzo3  9933  lbfzo0  9951  fzind2  10009  zmodid2  10118  redivap  10639  imdivap  10646  maxleast  10978  cosmul  11441  dfgcd2  11691  lcmneg  11744  coprmgcdb  11758  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  lmbrf  12373  uptx  12432  txcn  12433  xmetec  12595  bl2ioo  12700  findset  13132