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  4304  bnd2  4310  eqvinop  4383  copsexg  4384  uniuni  4597  rabxp  4812  elvvv  4838  rexiunxp  4922  resopab2  5110  ssrnres  5230  elxp4  5275  elxp5  5276  cnvresima  5277  mptpreima  5281  coass  5306  dff1o2  5644  eqfnfv3  5808  isoini  6024  f1oiso  6032  oprabid  6117  dfoprab2  6135  mpoeq123  6147  mpomptx  6179  resoprab2  6185  ovi3  6226  oprabex3  6362  spc2ed  6469  f1od2  6471  rexsupp  6493  brtpos2  6522  mapsnend  7099  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  ltexpi  7704  enq0enq  7798  enq0tr  7801  prnmaxl  7855  prnminu  7856  genpdflem  7874  ltexprlemm  7967  suplocsrlemb  8173  axaddf  8235  axmulf  8236  rexuz  9982  rexuz2  9983  rexrp  10079  elixx3g  10305  elfz2  10420  fzdifsuc  10490  fzind2  10660  sseqn  11281  hashfibclem  11284  divalgb  12694  gcdass  12794  nnwosdc  12818  lcmass  12865  isprm2  12897  infpn2  13349  fngzsum  13710  gzsumvalx  13711  issubg3  13997  dfrhm2  14463  ntreq0  15235  tx1cn  15372  tx2cn  15373  blres  15537  metrest  15609  elcncf1di  15682  dedekindicclemicc  15735  fsumdvdsmul  16111  lgsquadlem1  16208  lgsquadlem2  16209  wlk1walkdom  16612  isclwwlk  16647  isclwwlknx  16669  clwwlknonel  16685  clwwlknon2x  16688  iseupthf1o  16701  alsanmo  17163  ralsanmo  17164  2alsraln0m  17170