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  563  an32  564  an13  565  an31  566  an4  588  3anass  1008  sbidm  1898  4exdistr  1964  2sb5  2035  2sb5rf  2041  sbel2x  2050  r2exf  2549  r19.41  2687  ceqsex3v  2845  ceqsrex2v  2937  rexrab  2968  rexrab2  2972  rexss  3293  inass  3416  difin2  3468  difrab  3480  reupick3  3491  inssdif0im  3561  rexdifpr  3698  rexdifsn  3806  unidif0  4259  bnd2  4265  eqvinop  4337  copsexg  4338  uniuni  4550  rabxp  4765  elvvv  4791  rexiunxp  4874  resopab2  5062  ssrnres  5181  elxp4  5226  elxp5  5227  cnvresima  5228  mptpreima  5232  coass  5257  dff1o2  5591  eqfnfv3  5749  rexsupp  5774  isoini  5964  f1oiso  5972  oprabid  6055  dfoprab2  6073  mpoeq123  6085  mpomptx  6117  resoprab2  6123  ovi3  6164  oprabex3  6296  spc2ed  6403  f1od2  6405  brtpos2  6422  mapsnen  6991  xpsnen  7010  xpcomco  7015  xpassen  7019  ltexpi  7562  enq0enq  7656  enq0tr  7659  prnmaxl  7713  prnminu  7714  genpdflem  7732  ltexprlemm  7825  suplocsrlemb  8031  axaddf  8093  axmulf  8094  rexuz  9819  rexuz2  9820  rexrp  9916  elixx3g  10141  elfz2  10255  fzdifsuc  10321  fzind2  10491  divalgb  12509  gcdass  12609  nnwosdc  12633  lcmass  12680  isprm2  12712  infpn2  13100  fngsum  13494  igsumvalx  13495  issubg3  13802  dfrhm2  14192  ntreq0  14885  tx1cn  15022  tx2cn  15023  blres  15187  metrest  15259  elcncf1di  15332  dedekindicclemicc  15385  fsumdvdsmul  15744  lgsquadlem1  15835  lgsquadlem2  15836  wlk1walkdom  16239  isclwwlk  16274  isclwwlknx  16296  clwwlknonel  16312  clwwlknon2x  16315  iseupthf1o  16328