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  561  an32  562  an13  563  an31  564  an4  586  3anass  984  sbidm  1865  4exdistr  1931  2sb5  2002  2sb5rf  2008  sbel2x  2017  r2exf  2515  r19.41  2652  ceqsex3v  2806  ceqsrex2v  2896  rexrab  2927  rexrab2  2931  rexss  3251  inass  3374  difin2  3426  difrab  3438  reupick3  3449  inssdif0im  3519  rexdifpr  3651  rexdifsn  3755  unidif0  4201  bnd2  4207  eqvinop  4277  copsexg  4278  uniuni  4487  rabxp  4701  elvvv  4727  rexiunxp  4809  resopab2  4994  ssrnres  5113  elxp4  5158  elxp5  5159  cnvresima  5160  mptpreima  5164  coass  5189  dff1o2  5512  eqfnfv3  5664  rexsupp  5689  isoini  5868  f1oiso  5876  oprabid  5957  dfoprab2  5973  mpoeq123  5985  mpomptx  6017  resoprab2  6023  ovi3  6064  oprabex3  6195  spc2ed  6300  f1od2  6302  brtpos2  6318  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpassen  6898  ltexpi  7421  enq0enq  7515  enq0tr  7518  prnmaxl  7572  prnminu  7573  genpdflem  7591  ltexprlemm  7684  suplocsrlemb  7890  axaddf  7952  axmulf  7953  rexuz  9671  rexuz2  9672  rexrp  9768  elixx3g  9993  elfz2  10107  fzdifsuc  10173  fzind2  10332  divalgb  12107  gcdass  12207  nnwosdc  12231  lcmass  12278  isprm2  12310  infpn2  12698  fngsum  13090  igsumvalx  13091  issubg3  13398  dfrhm2  13786  ntreq0  14452  tx1cn  14589  tx2cn  14590  blres  14754  metrest  14826  elcncf1di  14899  dedekindicclemicc  14952  fsumdvdsmul  15311  lgsquadlem1  15402  lgsquadlem2  15403