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  9989  rexuz2  9990  rexrp  10087  elixx3g  10313  elfz2  10428  fzdifsuc  10498  fzind2  10668  sseqn  11293  hashfibclem  11296  divalgb  12708  gcdass  12808  nnwosdc  12832  lcmass  12879  isprm2  12911  infpn2  13396  fngzsum  13757  gzsumvalx  13758  issubg3  14044  dfrhm2  14510  ntreq0  15282  tx1cn  15419  tx2cn  15420  blres  15584  metrest  15656  elcncf1di  15729  dedekindicclemicc  15782  fsumdvdsmul  16186  lgsquadlem1  16294  lgsquadlem2  16295  wlk1walkdom  16698  isclwwlk  16733  isclwwlknx  16755  clwwlknonel  16771  clwwlknon2x  16774  iseupthf1o  16787  alsanmo  17249  ralsanmo  17250  2alsraln0m  17256