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  563  an32  564  an13  565  an31  566  an4  588  3anass  1009  sbidm  1899  4exdistr  1965  2sb5  2036  2sb5rf  2042  sbel2x  2051  r2exf  2551  r19.41  2689  ceqsex3v  2847  ceqsrex2v  2939  rexrab  2970  rexrab2  2974  rexss  3295  inass  3419  difin2  3471  difrab  3483  reupick3  3494  inssdif0im  3564  rexdifpr  3701  rexdifsn  3809  unidif0  4263  bnd2  4269  eqvinop  4341  copsexg  4342  uniuni  4554  rabxp  4769  elvvv  4795  rexiunxp  4878  resopab2  5066  ssrnres  5186  elxp4  5231  elxp5  5232  cnvresima  5233  mptpreima  5237  coass  5262  dff1o2  5597  eqfnfv3  5755  isoini  5969  f1oiso  5977  oprabid  6060  dfoprab2  6078  mpoeq123  6090  mpomptx  6122  resoprab2  6128  ovi3  6169  oprabex3  6300  spc2ed  6407  f1od2  6409  rexsupp  6431  brtpos2  6460  mapsnen  7029  xpsnen  7048  xpcomco  7053  xpassen  7057  ltexpi  7617  enq0enq  7711  enq0tr  7714  prnmaxl  7768  prnminu  7769  genpdflem  7787  ltexprlemm  7880  suplocsrlemb  8086  axaddf  8148  axmulf  8149  rexuz  9875  rexuz2  9876  rexrp  9972  elixx3g  10197  elfz2  10312  fzdifsuc  10378  fzind2  10548  divalgb  12566  gcdass  12666  nnwosdc  12690  lcmass  12737  isprm2  12769  infpn2  13157  fngsum  13551  igsumvalx  13552  issubg3  13859  dfrhm2  14249  ntreq0  14943  tx1cn  15080  tx2cn  15081  blres  15245  metrest  15317  elcncf1di  15390  dedekindicclemicc  15443  fsumdvdsmul  15805  lgsquadlem1  15896  lgsquadlem2  15897  wlk1walkdom  16300  isclwwlk  16335  isclwwlknx  16357  clwwlknonel  16373  clwwlknon2x  16376  iseupthf1o  16389