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  1862  4exdistr  1928  2sb5  1995  2sb5rf  2001  sbel2x  2010  r2exf  2508  r19.41  2645  ceqsex3v  2794  ceqsrex2v  2884  rexrab  2915  rexrab2  2919  rexss  3237  inass  3360  difin2  3412  difrab  3424  reupick3  3435  inssdif0im  3505  rexdifpr  3635  rexdifsn  3739  unidif0  4185  bnd2  4191  eqvinop  4261  copsexg  4262  uniuni  4469  rabxp  4681  elvvv  4707  rexiunxp  4787  resopab2  4972  ssrnres  5089  elxp4  5134  elxp5  5135  cnvresima  5136  mptpreima  5140  coass  5165  dff1o2  5485  eqfnfv3  5636  rexsupp  5661  isoini  5840  f1oiso  5848  oprabid  5928  dfoprab2  5943  mpoeq123  5955  mpomptx  5987  resoprab2  5993  ovi3  6033  oprabex3  6154  spc2ed  6258  f1od2  6260  brtpos2  6276  mapsnen  6837  xpsnen  6847  xpcomco  6852  xpassen  6856  ltexpi  7366  enq0enq  7460  enq0tr  7463  prnmaxl  7517  prnminu  7518  genpdflem  7536  ltexprlemm  7629  suplocsrlemb  7835  axaddf  7897  axmulf  7898  rexuz  9610  rexuz2  9611  rexrp  9706  elixx3g  9931  elfz2  10045  fzdifsuc  10111  fzind2  10269  divalgb  11962  gcdass  12048  nnwosdc  12072  lcmass  12117  isprm2  12149  infpn2  12507  issubg3  13131  dfrhm2  13504  ntreq0  14092  tx1cn  14229  tx2cn  14230  blres  14394  metrest  14466  elcncf1di  14526  dedekindicclemicc  14570