Theorem 3anass 1013

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 1011	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
2		anass 405	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
3	1, 2	bitri 184	1 |- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3736  rexdifpr  3737  trel3  4239  sowlin  4467  dff1o4  5650  mpoxopovel  6516  dfsmo2  6562  ecopovtrn  6910  ecopovtrng  6913  elixp2  6989  elixp  6992  mptelixpg  7021  eqinfti  7367  distrnqg  7761  recmulnqg  7765  ltexnqq  7782  enq0tr  7808  distrnq0  7833  genpdflem  7881  distrlem1prl  7956  distrlem1pru  7957  divmulasscomap  9035  muldivdirap  9046  divmuldivap  9051  prime  9757  eluz2  9944  raluz2  9996  elixx1  10317  elixx3g  10321  elioo2  10341  elioo5  10353  elicc4  10360  iccneg  10409  icoshft  10410  elfz1  10434  elfz  10435  elfz2  10436  elfzm11  10516  elfz2nn0  10537  elfzo2  10575  elfzo3  10589  lbfzo0  10610  fzind2  10676  zmodid2  10811  swrdccatin1  11520  swrdccat  11530  redivap  11662  imdivap  11669  maxleast  12003  cosmul  12538  bitsval  12736  bitsmod  12749  bitscmp  12751  dfgcd2  12817  lcmneg  12878  coprmgcdb  12892  divgcdcoprmex  12906  cncongr1  12907  cncongr2  12908  difsqpwdvds  13147  elgz  13180  xpsfrnel  13725  xpsfrnel2  13727  mgmsscl  13741  ismhm  13828  mhmpropd  13833  issubm  13839  issubg  14036  eqglact  14088  eqgid  14089  ecqusaddd  14101  ecqusaddcl  14102  isrng  14341  issrg  14377  srglmhm  14405  srgrmhm  14406  isring  14412  ringlghm  14474  dfrhm2  14571  issubrng  14617  issubrg3  14665  islmod  14737  islssm  14804  islssmg  14805  lsspropdg  14878  qusmulrng  14979  lmbrf  15453  uptx  15512  txcn  15513  xmetec  15675  bl2ioo  15788  lgsmodeq  16381  lgsmulsqcoprm  16382  uspgredg2v  16679  wksfval  16780  wlkeq  16812  isclwwlk  16852  clwwlkbp  16853  isclwwlknx  16874  clwwlknp  16875  clwwlkn1  16876  clwwlkn2  16879  clwwlknonel  16890  findset  17188