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  1865  4exdistr  1931  2sb5  2002  2sb5rf  2008  sbel2x  2017  r2exf  2515  r19.41  2652  ceqsex3v  2806  ceqsrex2v  2896  rexrab  2927  rexrab2  2931  rexss  3250  inass  3373  difin2  3425  difrab  3437  reupick3  3448  inssdif0im  3518  rexdifpr  3650  rexdifsn  3754  unidif0  4200  bnd2  4206  eqvinop  4276  copsexg  4277  uniuni  4486  rabxp  4700  elvvv  4726  rexiunxp  4808  resopab2  4993  ssrnres  5112  elxp4  5157  elxp5  5158  cnvresima  5159  mptpreima  5163  coass  5188  dff1o2  5509  eqfnfv3  5661  rexsupp  5686  isoini  5865  f1oiso  5873  oprabid  5954  dfoprab2  5969  mpoeq123  5981  mpomptx  6013  resoprab2  6019  ovi3  6060  oprabex3  6186  spc2ed  6291  f1od2  6293  brtpos2  6309  mapsnen  6870  xpsnen  6880  xpcomco  6885  xpassen  6889  ltexpi  7404  enq0enq  7498  enq0tr  7501  prnmaxl  7555  prnminu  7556  genpdflem  7574  ltexprlemm  7667  suplocsrlemb  7873  axaddf  7935  axmulf  7936  rexuz  9654  rexuz2  9655  rexrp  9751  elixx3g  9976  elfz2  10090  fzdifsuc  10156  fzind2  10315  divalgb  12090  gcdass  12182  nnwosdc  12206  lcmass  12253  isprm2  12285  infpn2  12673  fngsum  13031  igsumvalx  13032  issubg3  13322  dfrhm2  13710  ntreq0  14368  tx1cn  14505  tx2cn  14506  blres  14670  metrest  14742  elcncf1di  14815  dedekindicclemicc  14868  fsumdvdsmul  15227  lgsquadlem1  15318  lgsquadlem2  15319