Theorem anass 401

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 400	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 19	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 399	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 126	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 104   <-> wb 105

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

This theorem is referenced by:  bianass  469  mpan10  474  an12  563  an32  564  an13  565  an31  566  an4  588  3anass  1009  sbidm  1900  4exdistr  1968  2sb5  2039  2sb5rf  2045  sbel2x  2054  r2exf  2562  r19.41  2700  ceqsex3v  2859  ceqsrex2v  2952  rexrab  2983  rexrab2  2987  rexss  3309  inass  3435  difin2  3487  difrab  3499  reupick3  3510  inssdif0im  3580  rexdifpr  3722  rexdifsn  3830  unidif0  4285  bnd2  4291  eqvinop  4364  copsexg  4365  uniuni  4577  rabxp  4792  elvvv  4818  rexiunxp  4902  resopab2  5090  ssrnres  5210  elxp4  5255  elxp5  5256  cnvresima  5257  mptpreima  5261  coass  5286  dff1o2  5624  eqfnfv3  5782  isoini  5997  f1oiso  6005  oprabid  6090  dfoprab2  6108  mpoeq123  6120  mpomptx  6152  resoprab2  6158  ovi3  6199  oprabex3  6335  spc2ed  6442  f1od2  6444  rexsupp  6466  brtpos2  6495  mapsnend  7065  mapsnen  7066  xpsnen  7085  xpcomco  7090  xpassen  7094  ltexpi  7668  enq0enq  7762  enq0tr  7765  prnmaxl  7819  prnminu  7820  genpdflem  7838  ltexprlemm  7931  suplocsrlemb  8137  axaddf  8199  axmulf  8200  rexuz  9933  rexuz2  9934  rexrp  10030  elixx3g  10256  elfz2  10371  fzdifsuc  10440  fzind2  10610  sseqn  11231  hashfibclem  11234  divalgb  12639  gcdass  12739  nnwosdc  12763  lcmass  12810  isprm2  12842  infpn2  13294  fngsum  13654  igsumvalx  13655  issubg3  13948  dfrhm2  14402  ntreq0  15126  tx1cn  15263  tx2cn  15264  blres  15428  metrest  15500  elcncf1di  15573  dedekindicclemicc  15626  fsumdvdsmul  15988  lgsquadlem1  16079  lgsquadlem2  16080  wlk1walkdom  16483  isclwwlk  16518  isclwwlknx  16540  clwwlknonel  16556  clwwlknon2x  16559  iseupthf1o  16572