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  982  sbidm  1851  4exdistr  1916  2sb5  1983  2sb5rf  1989  sbel2x  1998  r2exf  2495  r19.41  2632  ceqsex3v  2781  ceqsrex2v  2871  rexrab  2902  rexrab2  2906  rexss  3224  inass  3347  difin2  3399  difrab  3411  reupick3  3422  inssdif0im  3492  rexdifpr  3622  rexdifsn  3726  unidif0  4169  bnd2  4175  eqvinop  4245  copsexg  4246  uniuni  4453  rabxp  4665  elvvv  4691  rexiunxp  4771  resopab2  4956  ssrnres  5073  elxp4  5118  elxp5  5119  cnvresima  5120  mptpreima  5124  coass  5149  dff1o2  5468  eqfnfv3  5617  rexsupp  5642  isoini  5821  f1oiso  5829  oprabid  5909  dfoprab2  5924  mpoeq123  5936  mpomptx  5968  resoprab2  5974  ovi3  6013  oprabex3  6132  spc2ed  6236  f1od2  6238  brtpos2  6254  mapsnen  6813  xpsnen  6823  xpcomco  6828  xpassen  6832  ltexpi  7338  enq0enq  7432  enq0tr  7435  prnmaxl  7489  prnminu  7490  genpdflem  7508  ltexprlemm  7601  suplocsrlemb  7807  axaddf  7869  axmulf  7870  rexuz  9582  rexuz2  9583  rexrp  9678  elixx3g  9903  elfz2  10017  fzdifsuc  10083  fzind2  10241  divalgb  11932  gcdass  12018  nnwosdc  12042  lcmass  12087  isprm2  12119  infpn2  12459  issubg3  13057  ntreq0  13671  tx1cn  13808  tx2cn  13809  blres  13973  metrest  14045  elcncf1di  14105  dedekindicclemicc  14149