Theorem anass 393

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

Syntax hints:   ∧ wa 102   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpan10  458  an12  526  an32  527  an13  528  an31  529  an4  551  3anass  924  sbidm  1773  4exdistr  1835  2sb5  1901  2sb5rf  1907  sbel2x  1916  r2exf  2385  r19.41  2510  ceqsex3v  2642  ceqsrex2v  2728  rexrab  2756  rexrab2  2760  rexss  3062  inass  3177  difin2  3227  difrab  3239  reupick3  3250  inssdif0im  3312  rexdifsn  3523  unidif0  3943  bnd2  3949  eqvinop  4000  copsexg  4001  uniuni  4203  rabxp  4400  elvvv  4423  rexiunxp  4500  resopab2  4679  ssrnres  4787  elxp4  4832  elxp5  4833  cnvresima  4834  mptpreima  4838  coass  4863  dff1o2  5156  eqfnfv3  5293  rexsupp  5317  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  6355  xpcomco  6360  xpassen  6364  ltexpi  6578  enq0enq  6672  enq0tr  6675  prnmaxl  6729  prnminu  6730  genpdflem  6748  ltexprlemm  6841  rexuz  8738  rexuz2  8739  rexrp  8826  elixx3g  8989  elfz2  9101  fzdifsuc  9163  fzind2  9314  divalgb  10458  gcdass  10537  lcmass  10600  isprm2  10632