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  1966  2sb5  2037  2sb5rf  2043  sbel2x  2052  r2exf  2560  r19.41  2698  ceqsex3v  2856  ceqsrex2v  2948  rexrab  2979  rexrab2  2983  rexss  3304  inass  3430  difin2  3482  difrab  3494  reupick3  3505  inssdif0im  3575  rexdifpr  3716  rexdifsn  3824  unidif0  4279  bnd2  4285  eqvinop  4358  copsexg  4359  uniuni  4571  rabxp  4786  elvvv  4812  rexiunxp  4896  resopab2  5084  ssrnres  5204  elxp4  5249  elxp5  5250  cnvresima  5251  mptpreima  5255  coass  5280  dff1o2  5618  eqfnfv3  5776  isoini  5990  f1oiso  5998  oprabid  6081  dfoprab2  6099  mpoeq123  6111  mpomptx  6143  resoprab2  6149  ovi3  6190  oprabex3  6321  spc2ed  6428  f1od2  6430  rexsupp  6452  brtpos2  6481  mapsnend  7051  mapsnen  7052  xpsnen  7071  xpcomco  7076  xpassen  7080  ltexpi  7648  enq0enq  7742  enq0tr  7745  prnmaxl  7799  prnminu  7800  genpdflem  7818  ltexprlemm  7911  suplocsrlemb  8117  axaddf  8179  axmulf  8180  rexuz  9908  rexuz2  9909  rexrp  10005  elixx3g  10230  elfz2  10345  fzdifsuc  10411  fzind2  10581  sseqn  11196  hashfibclem  11199  divalgb  12604  gcdass  12704  nnwosdc  12728  lcmass  12775  isprm2  12807  infpn2  13196  fngsum  13590  igsumvalx  13591  issubg3  13898  dfrhm2  14288  ntreq0  14984  tx1cn  15121  tx2cn  15122  blres  15286  metrest  15358  elcncf1di  15431  dedekindicclemicc  15484  fsumdvdsmul  15846  lgsquadlem1  15937  lgsquadlem2  15938  wlk1walkdom  16341  isclwwlk  16376  isclwwlknx  16398  clwwlknonel  16414  clwwlknon2x  16417  iseupthf1o  16430