Theorem anass 387

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

Syntax hints:   ∧ wa 101   ↔ wb 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  mpan10  451  an12  503  an32  504  an13  505  an31  506  an4  528  3anass  898  sbidm  1745  4exdistr  1807  2sb5  1873  2sb5rf  1879  sbel2x  1888  r2exf  2357  r19.41  2480  ceqsex3v  2611  ceqsrex2v  2696  rexrab  2724  rexrab2  2728  rexss  3032  inass  3172  difin2  3224  difrab  3236  reupick3  3247  inssdif0im  3316  rexdifsn  3524  unidif0  3945  bnd2  3951  eqvinop  4005  copsexg  4006  uniuni  4208  rabxp  4405  elvvv  4428  rexiunxp  4503  resopab2  4680  ssrnres  4788  elxp4  4833  elxp5  4834  cnvresima  4835  mptpreima  4839  coass  4864  dff1o2  5156  eqfnfv3  5292  rexsupp  5316  isoini  5482  f1oiso  5490  oprabid  5562  dfoprab2  5577  mpt2eq123  5589  mpt2mptx  5620  resoprab2  5623  ovi3  5662  oprabex3  5781  spc2ed  5879  f1od2  5881  brtpos2  5894  xpsnen  6323  xpcomco  6328  xpassen  6332  ltexpi  6463  enq0enq  6557  enq0tr  6560  prnmaxl  6614  prnminu  6615  genpdflem  6633  ltexprlemm  6726  rexuz  8589  rexuz2  8590  rexrp  8673  elixx3g  8841  elfz2  8953  fzdifsuc  9015  fzind2  9167