Theorem anass 405

Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Assertion

Ref	Expression
anass	|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ph /\ ( ps /\ ch ) ) )
2	1	anassrs 404	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 19	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 403	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 126	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

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

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

This theorem is used by:  bianass  473  mpan10  478  an12  567  an32  568  an13  569  an31  570  an4  592  3anass  1013  sbidm  1904  4exdistr  1972  2sb5  2043  2sb5rf  2049  sbel2x  2058  r2exf  2568  r19.41  2706  ceqsex3v  2865  ceqsrex2v  2958  rexrab  2989  rexrab2  2993  rexss  3315  inass  3441  difin2  3493  difrab  3507  reupick3  3518  inssdif0imOLD  3593  rexdifpr  3737  rexdifsn  3846  unidif0  4306  bnd2  4312  eqvinop  4385  copsexg  4386  uniuni  4599  rabxp  4814  elvvv  4840  rexiunxp  4924  resopab2  5113  ssrnres  5233  elxp4  5278  elxp5  5279  cnvresima  5280  mptpreima  5284  coass  5309  dff1o2  5647  eqfnfv3  5811  isoini  6027  f1oiso  6035  oprabid  6120  dfoprab2  6138  mpoeq123  6150  mpomptx  6182  resoprab2  6188  ovi3  6229  oprabex3  6366  spc2ed  6473  f1od2  6475  rexsupp  6497  brtpos2  6527  mapsnend  7105  mapsnen  7106  xpsnen  7125  xpcomco  7130  xpassen  7134  ltexpi  7711  enq0enq  7805  enq0tr  7808  prnmaxl  7862  prnminu  7863  genpdflem  7881  ltexprlemm  7974  suplocsrlemb  8180  axaddf  8242  axmulf  8243  rexuz  9996  rexuz2  9997  rexrp  10094  elixx3g  10320  elfz2  10435  fzdifsuc  10505  fzind2  10675  sseqn  11301  hashfibclem  11304  divalgb  12717  gcdass  12817  nnwosdc  12841  lcmass  12888  isprm2  12920  infpn2  13405  fngzsum  13767  gzsumvalx  13768  issubg3  14054  resscntz  14166  dfrhm2  14570  ntreq0  15391  tx1cn  15528  tx2cn  15529  blres  15693  metrest  15765  elcncf1di  15838  dedekindicclemicc  15891  fsumdvdsmul  16318  lgsquadlem1  16434  lgsquadlem2  16435  wlk1walkdom  16838  isclwwlk  16873  isclwwlknx  16895  clwwlknonel  16911  clwwlknon2x  16914  iseupthf1o  16927  idjudju  17285  alsanmo  17391  ralsanmo  17392  2alsraln0m  17398