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  2951  rexrab  2982  rexrab2  2986  rexss  3307  inass  3433  difin2  3485  difrab  3497  reupick3  3508  inssdif0im  3578  rexdifpr  3719  rexdifsn  3827  unidif0  4282  bnd2  4288  eqvinop  4361  copsexg  4362  uniuni  4574  rabxp  4789  elvvv  4815  rexiunxp  4899  resopab2  5087  ssrnres  5207  elxp4  5252  elxp5  5253  cnvresima  5254  mptpreima  5258  coass  5283  dff1o2  5621  eqfnfv3  5779  isoini  5993  f1oiso  6001  oprabid  6084  dfoprab2  6102  mpoeq123  6114  mpomptx  6146  resoprab2  6152  ovi3  6193  oprabex3  6324  spc2ed  6431  f1od2  6433  rexsupp  6455  brtpos2  6484  mapsnend  7054  mapsnen  7055  xpsnen  7074  xpcomco  7079  xpassen  7083  ltexpi  7657  enq0enq  7751  enq0tr  7754  prnmaxl  7808  prnminu  7809  genpdflem  7827  ltexprlemm  7920  suplocsrlemb  8126  axaddf  8188  axmulf  8189  rexuz  9918  rexuz2  9919  rexrp  10015  elixx3g  10240  elfz2  10355  fzdifsuc  10422  fzind2  10592  sseqn  11211  hashfibclem  11214  divalgb  12619  gcdass  12719  nnwosdc  12743  lcmass  12790  isprm2  12822  infpn2  13228  fngsum  13622  igsumvalx  13623  issubg3  13930  dfrhm2  14321  ntreq0  15046  tx1cn  15183  tx2cn  15184  blres  15348  metrest  15420  elcncf1di  15493  dedekindicclemicc  15546  fsumdvdsmul  15908  lgsquadlem1  15999  lgsquadlem2  16000  wlk1walkdom  16403  isclwwlk  16438  isclwwlknx  16460  clwwlknonel  16476  clwwlknon2x  16479  iseupthf1o  16492