Theorem anass 405

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 404	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 19	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 403	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 126	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bianass  473  mpan10  478  an12  567  an32  568  an13  569  an31  570  an4  592  3anass  1013  sbidm  1904  4exdistr  1972  2sb5  2043  2sb5rf  2049  sbel2x  2058  r2exf  2568  r19.41  2706  ceqsex3v  2865  ceqsrex2v  2958  rexrab  2989  rexrab2  2993  rexss  3315  inass  3441  difin2  3493  difrab  3507  reupick3  3518  inssdif0imOLD  3593  rexdifpr  3737  rexdifsn  3846  unidif0  4304  bnd2  4310  eqvinop  4383  copsexg  4384  uniuni  4597  rabxp  4812  elvvv  4838  rexiunxp  4922  resopab2  5110  ssrnres  5230  elxp4  5275  elxp5  5276  cnvresima  5277  mptpreima  5281  coass  5306  dff1o2  5644  eqfnfv3  5808  isoini  6024  f1oiso  6032  oprabid  6117  dfoprab2  6135  mpoeq123  6147  mpomptx  6179  resoprab2  6185  ovi3  6226  oprabex3  6362  spc2ed  6469  f1od2  6471  rexsupp  6493  brtpos2  6522  mapsnend  7099  mapsnen  7100  xpsnen  7119  xpcomco  7124  xpassen  7128  ltexpi  7705  enq0enq  7799  enq0tr  7802  prnmaxl  7856  prnminu  7857  genpdflem  7875  ltexprlemm  7968  suplocsrlemb  8174  axaddf  8236  axmulf  8237  rexuz  9990  rexuz2  9991  rexrp  10088  elixx3g  10314  elfz2  10429  fzdifsuc  10499  fzind2  10669  sseqn  11295  hashfibclem  11298  divalgb  12711  gcdass  12811  nnwosdc  12835  lcmass  12882  isprm2  12914  infpn2  13399  fngzsum  13761  gzsumvalx  13762  issubg3  14048  resscntz  14160  dfrhm2  14545  ntreq0  15324  tx1cn  15461  tx2cn  15462  blres  15626  metrest  15698  elcncf1di  15771  dedekindicclemicc  15824  fsumdvdsmul  16246  lgsquadlem1  16362  lgsquadlem2  16363  wlk1walkdom  16766  isclwwlk  16801  isclwwlknx  16823  clwwlknonel  16839  clwwlknon2x  16842  iseupthf1o  16855  alsanmo  17318  ralsanmo  17319  2alsraln0m  17325