Theorem anass 381

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

Syntax hints:   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  mpan10  443  an12  495  an32  496  an13  497  an31  498  an4  520  3anass  889  sbidm  1731  4exdistr  1793  2sb5  1859  2sb5rf  1865  sbel2x  1874  r2exf  2342  r19.41  2465  ceqsex3v  2596  ceqsrex2v  2676  rexrab  2704  rexrab2  2708  rexss  3007  inass  3147  difin2  3199  difrab  3211  reupick3  3222  inssdif0im  3291  rexdifsn  3499  unidif0  3920  bnd2  3926  eqvinop  3980  copsexg  3981  uniuni  4183  rabxp  4380  elvvv  4403  rexiunxp  4478  resopab2  4655  ssrnres  4763  elxp4  4808  elxp5  4809  cnvresima  4810  mptpreima  4814  coass  4839  dff1o2  5131  eqfnfv3  5267  rexsupp  5291  isoini  5457  f1oiso  5465  oprabid  5537  dfoprab2  5552  mpt2eq123  5564  mpt2mptx  5595  resoprab2  5598  ovi3  5637  oprabex3  5756  brtpos2  5866  xpsnen  6295  xpcomco  6300  xpassen  6304  ltexpi  6435  enq0enq  6529  enq0tr  6532  prnmaxl  6586  prnminu  6587  genpdflem  6605  ltexprlemm  6698  rexuz  8523  rexuz2  8524  rexrp  8605  elixx3g  8770  elfz2  8881  fzdifsuc  8943  fzind2  9095