Theorem anass 399

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 398	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ph /\ ( ps /\ ch ) ) )
3		id 19	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> ( ( ph /\ ps ) /\ ch ) )
4	3	anasss 397	. 2 |- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) /\ ch ) )
5	2, 4	impbii 125	1 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )

Syntax hints:   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bianass  466  mpan10  471  an12  556  an32  557  an13  558  an31  559  an4  581  3anass  977  sbidm  1844  4exdistr  1909  2sb5  1976  2sb5rf  1982  sbel2x  1991  r2exf  2488  r19.41  2625  ceqsex3v  2772  ceqsrex2v  2862  rexrab  2893  rexrab2  2897  rexss  3214  inass  3337  difin2  3389  difrab  3401  reupick3  3412  inssdif0im  3482  rexdifpr  3611  rexdifsn  3715  unidif0  4153  bnd2  4159  eqvinop  4228  copsexg  4229  uniuni  4436  rabxp  4648  elvvv  4674  rexiunxp  4753  resopab2  4938  ssrnres  5053  elxp4  5098  elxp5  5099  cnvresima  5100  mptpreima  5104  coass  5129  dff1o2  5447  eqfnfv3  5595  rexsupp  5620  isoini  5797  f1oiso  5805  oprabid  5885  dfoprab2  5900  mpoeq123  5912  mpomptx  5944  resoprab2  5950  ovi3  5989  oprabex3  6108  spc2ed  6212  f1od2  6214  brtpos2  6230  mapsnen  6789  xpsnen  6799  xpcomco  6804  xpassen  6808  ltexpi  7299  enq0enq  7393  enq0tr  7396  prnmaxl  7450  prnminu  7451  genpdflem  7469  ltexprlemm  7562  suplocsrlemb  7768  axaddf  7830  axmulf  7831  rexuz  9539  rexuz2  9540  rexrp  9633  elixx3g  9858  elfz2  9972  fzdifsuc  10037  fzind2  10195  divalgb  11884  gcdass  11970  nnwosdc  11994  lcmass  12039  isprm2  12071  infpn2  12411  ntreq0  12926  tx1cn  13063  tx2cn  13064  blres  13228  metrest  13300  elcncf1di  13360  dedekindicclemicc  13404