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  7705  enq0enq  7799  enq0tr  7802  prnmaxl  7856  prnminu  7857  genpdflem  7875  ltexprlemm  7968  suplocsrlemb  8174  axaddf  8236  axmulf  8237  rexuz  9990  rexuz2  9991  rexrp  10088  elixx3g  10314  elfz2  10429  fzdifsuc  10499  fzind2  10669  sseqn  11294  hashfibclem  11297  divalgb  12710  gcdass  12810  nnwosdc  12834  lcmass  12881  isprm2  12913  infpn2  13398  fngzsum  13759  gzsumvalx  13760  issubg3  14046  dfrhm2  14512  ntreq0  15285  tx1cn  15422  tx2cn  15423  blres  15587  metrest  15659  elcncf1di  15732  dedekindicclemicc  15785  fsumdvdsmul  16207  lgsquadlem1  16318  lgsquadlem2  16319  wlk1walkdom  16722  isclwwlk  16757  isclwwlknx  16779  clwwlknonel  16795  clwwlknon2x  16798  iseupthf1o  16811  alsanmo  17273  ralsanmo  17274  2alsraln0m  17280