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  4306  bnd2  4312  eqvinop  4385  copsexg  4386  uniuni  4599  rabxp  4814  elvvv  4840  rexiunxp  4924  resopab2  5113  ssrnres  5233  elxp4  5278  elxp5  5279  cnvresima  5280  mptpreima  5284  coass  5309  dff1o2  5647  eqfnfv3  5811  isoini  6027  f1oiso  6035  oprabid  6120  dfoprab2  6138  mpoeq123  6150  mpomptx  6182  resoprab2  6188  ovi3  6229  oprabex3  6366  spc2ed  6473  f1od2  6475  rexsupp  6497  brtpos2  6526  mapsnend  7104  mapsnen  7105  xpsnen  7124  xpcomco  7129  xpassen  7133  ltexpi  7711  enq0enq  7805  enq0tr  7808  prnmaxl  7862  prnminu  7863  genpdflem  7881  ltexprlemm  7974  suplocsrlemb  8180  axaddf  8242  axmulf  8243  rexuz  9997  rexuz2  9998  rexrp  10095  elixx3g  10321  elfz2  10436  fzdifsuc  10506  fzind2  10676  sseqn  11302  hashfibclem  11305  divalgb  12718  gcdass  12818  nnwosdc  12842  lcmass  12889  isprm2  12921  infpn2  13406  fngzsum  13768  gzsumvalx  13769  issubg3  14055  resscntz  14167  dfrhm2  14571  ntreq0  15370  tx1cn  15507  tx2cn  15508  blres  15672  metrest  15744  elcncf1di  15817  dedekindicclemicc  15870  fsumdvdsmul  16297  lgsquadlem1  16413  lgsquadlem2  16414  wlk1walkdom  16817  isclwwlk  16852  isclwwlknx  16874  clwwlknonel  16890  clwwlknon2x  16893  iseupthf1o  16906  idjudju  17264  alsanmo  17370  ralsanmo  17371  2alsraln0m  17377