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 ) ) )

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  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  3736  rexdifsn  3844  unidif0  4302  bnd2  4308  eqvinop  4381  copsexg  4382  uniuni  4595  rabxp  4810  elvvv  4836  rexiunxp  4920  resopab2  5108  ssrnres  5228  elxp4  5273  elxp5  5274  cnvresima  5275  mptpreima  5279  coass  5304  dff1o2  5642  eqfnfv3  5802  isoini  6018  f1oiso  6026  oprabid  6111  dfoprab2  6129  mpoeq123  6141  mpomptx  6173  resoprab2  6179  ovi3  6220  oprabex3  6356  spc2ed  6463  f1od2  6465  rexsupp  6487  brtpos2  6516  mapsnend  7093  mapsnen  7094  xpsnen  7113  xpcomco  7118  xpassen  7122  ltexpi  7698  enq0enq  7792  enq0tr  7795  prnmaxl  7849  prnminu  7850  genpdflem  7868  ltexprlemm  7961  suplocsrlemb  8167  axaddf  8229  axmulf  8230  rexuz  9963  rexuz2  9964  rexrp  10060  elixx3g  10286  elfz2  10401  fzdifsuc  10471  fzind2  10641  sseqn  11262  hashfibclem  11265  divalgb  12675  gcdass  12775  nnwosdc  12799  lcmass  12846  isprm2  12878  infpn2  13330  fngzsum  13691  gzsumvalx  13692  issubg3  13978  dfrhm2  14444  ntreq0  15216  tx1cn  15353  tx2cn  15354  blres  15518  metrest  15590  elcncf1di  15663  dedekindicclemicc  15716  fsumdvdsmul  16088  lgsquadlem1  16179  lgsquadlem2  16180  wlk1walkdom  16583  isclwwlk  16618  isclwwlknx  16640  clwwlknonel  16656  clwwlknon2x  16659  iseupthf1o  16672  alsanmo  17125  ralsanmo  17126  2alsraln0m  17132