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  561  an32  562  an13  563  an31  564  an4  586  3anass  985  sbidm  1874  4exdistr  1940  2sb5  2011  2sb5rf  2017  sbel2x  2026  r2exf  2524  r19.41  2661  ceqsex3v  2815  ceqsrex2v  2905  rexrab  2936  rexrab2  2940  rexss  3260  inass  3383  difin2  3435  difrab  3447  reupick3  3458  inssdif0im  3528  rexdifpr  3661  rexdifsn  3765  unidif0  4212  bnd2  4218  eqvinop  4288  copsexg  4289  uniuni  4499  rabxp  4713  elvvv  4739  rexiunxp  4821  resopab2  5007  ssrnres  5126  elxp4  5171  elxp5  5172  cnvresima  5173  mptpreima  5177  coass  5202  dff1o2  5529  eqfnfv3  5681  rexsupp  5706  isoini  5889  f1oiso  5897  oprabid  5978  dfoprab2  5994  mpoeq123  6006  mpomptx  6038  resoprab2  6044  ovi3  6085  oprabex3  6216  spc2ed  6321  f1od2  6323  brtpos2  6339  mapsnen  6905  xpsnen  6918  xpcomco  6923  xpassen  6927  ltexpi  7452  enq0enq  7546  enq0tr  7549  prnmaxl  7603  prnminu  7604  genpdflem  7622  ltexprlemm  7715  suplocsrlemb  7921  axaddf  7983  axmulf  7984  rexuz  9703  rexuz2  9704  rexrp  9800  elixx3g  10025  elfz2  10139  fzdifsuc  10205  fzind2  10370  divalgb  12269  gcdass  12369  nnwosdc  12393  lcmass  12440  isprm2  12472  infpn2  12860  fngsum  13253  igsumvalx  13254  issubg3  13561  dfrhm2  13949  ntreq0  14637  tx1cn  14774  tx2cn  14775  blres  14939  metrest  15011  elcncf1di  15084  dedekindicclemicc  15137  fsumdvdsmul  15496  lgsquadlem1  15587  lgsquadlem2  15588