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	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		id 19	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
2	1	anassrs 400	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 19	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 399	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 126	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

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  3638  rexdifsn  3742  unidif0  4188  bnd2  4194  eqvinop  4264  copsexg  4265  uniuni  4472  rabxp  4684  elvvv  4710  rexiunxp  4790  resopab2  4975  ssrnres  5092  elxp4  5137  elxp5  5138  cnvresima  5139  mptpreima  5143  coass  5168  dff1o2  5488  eqfnfv3  5639  rexsupp  5664  isoini  5843  f1oiso  5851  oprabid  5932  dfoprab2  5947  mpoeq123  5959  mpomptx  5991  resoprab2  5997  ovi3  6037  oprabex3  6158  spc2ed  6262  f1od2  6264  brtpos2  6280  mapsnen  6841  xpsnen  6851  xpcomco  6856  xpassen  6860  ltexpi  7371  enq0enq  7465  enq0tr  7468  prnmaxl  7522  prnminu  7523  genpdflem  7541  ltexprlemm  7634  suplocsrlemb  7840  axaddf  7902  axmulf  7903  rexuz  9616  rexuz2  9617  rexrp  9712  elixx3g  9937  elfz2  10051  fzdifsuc  10117  fzind2  10275  divalgb  11971  gcdass  12057  nnwosdc  12081  lcmass  12128  isprm2  12160  infpn2  12518  fngsum  12875  igsumvalx  12876  issubg3  13156  dfrhm2  13529  ntreq0  14117  tx1cn  14254  tx2cn  14255  blres  14419  metrest  14491  elcncf1di  14551  dedekindicclemicc  14595