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  7704  enq0enq  7798  enq0tr  7801  prnmaxl  7855  prnminu  7856  genpdflem  7874  ltexprlemm  7967  suplocsrlemb  8173  axaddf  8235  axmulf  8236  rexuz  9980  rexuz2  9981  rexrp  10077  elixx3g  10303  elfz2  10418  fzdifsuc  10488  fzind2  10658  sseqn  11279  hashfibclem  11282  divalgb  12692  gcdass  12792  nnwosdc  12816  lcmass  12863  isprm2  12895  infpn2  13347  fngzsum  13708  gzsumvalx  13709  issubg3  13995  dfrhm2  14461  ntreq0  15233  tx1cn  15370  tx2cn  15371  blres  15535  metrest  15607  elcncf1di  15680  dedekindicclemicc  15733  fsumdvdsmul  16105  lgsquadlem1  16196  lgsquadlem2  16197  wlk1walkdom  16600  isclwwlk  16635  isclwwlknx  16657  clwwlknonel  16673  clwwlknon2x  16676  iseupthf1o  16689  alsanmo  17151  ralsanmo  17152  2alsraln0m  17158