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  1899  4exdistr  1965  2sb5  2036  2sb5rf  2042  sbel2x  2051  r2exf  2550  r19.41  2688  ceqsex3v  2846  ceqsrex2v  2938  rexrab  2969  rexrab2  2973  rexss  3294  inass  3417  difin2  3469  difrab  3481  reupick3  3492  inssdif0im  3562  rexdifpr  3697  rexdifsn  3805  unidif0  4257  bnd2  4263  eqvinop  4335  copsexg  4336  uniuni  4548  rabxp  4763  elvvv  4789  rexiunxp  4872  resopab2  5060  ssrnres  5179  elxp4  5224  elxp5  5225  cnvresima  5226  mptpreima  5230  coass  5255  dff1o2  5588  eqfnfv3  5746  rexsupp  5771  isoini  5959  f1oiso  5967  oprabid  6050  dfoprab2  6068  mpoeq123  6080  mpomptx  6112  resoprab2  6118  ovi3  6159  oprabex3  6291  spc2ed  6398  f1od2  6400  brtpos2  6417  mapsnen  6986  xpsnen  7005  xpcomco  7010  xpassen  7014  ltexpi  7557  enq0enq  7651  enq0tr  7654  prnmaxl  7708  prnminu  7709  genpdflem  7727  ltexprlemm  7820  suplocsrlemb  8026  axaddf  8088  axmulf  8089  rexuz  9814  rexuz2  9815  rexrp  9911  elixx3g  10136  elfz2  10250  fzdifsuc  10316  fzind2  10485  divalgb  12487  gcdass  12587  nnwosdc  12611  lcmass  12658  isprm2  12690  infpn2  13078  fngsum  13472  igsumvalx  13473  issubg3  13780  dfrhm2  14170  ntreq0  14858  tx1cn  14995  tx2cn  14996  blres  15160  metrest  15232  elcncf1di  15305  dedekindicclemicc  15358  fsumdvdsmul  15717  lgsquadlem1  15808  lgsquadlem2  15809  wlk1walkdom  16212  isclwwlk  16247  isclwwlknx  16269  clwwlknonel  16285  clwwlknon2x  16288  iseupthf1o  16301