Theorem anass 394

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpan10  459  an12  529  an32  530  an13  531  an31  532  an4  554  3anass  931  sbidm  1786  4exdistr  1848  2sb5  1914  2sb5rf  1920  sbel2x  1929  r2exf  2407  r19.41  2536  ceqsex3v  2675  ceqsrex2v  2763  rexrab  2792  rexrab2  2796  rexss  3103  inass  3225  difin2  3277  difrab  3289  reupick3  3300  inssdif0im  3369  rexdifsn  3594  unidif0  4023  bnd2  4029  eqvinop  4094  copsexg  4095  uniuni  4301  rabxp  4504  elvvv  4530  rexiunxp  4609  resopab2  4792  ssrnres  4907  elxp4  4952  elxp5  4953  cnvresima  4954  mptpreima  4958  coass  4983  dff1o2  5293  eqfnfv3  5438  rexsupp  5462  isoini  5635  f1oiso  5643  oprabid  5719  dfoprab2  5734  mpt2eq123  5746  mpt2mptx  5777  resoprab2  5780  ovi3  5819  oprabex3  5938  spc2ed  6036  f1od2  6038  brtpos2  6054  mapsnen  6608  xpsnen  6617  xpcomco  6622  xpassen  6626  ltexpi  6993  enq0enq  7087  enq0tr  7090  prnmaxl  7144  prnminu  7145  genpdflem  7163  ltexprlemm  7256  rexuz  9167  rexuz2  9168  rexrp  9255  elixx3g  9467  elfz2  9580  fzdifsuc  9644  fzind2  9799  divalgb  11352  gcdass  11431  lcmass  11494  isprm2  11526  ntreq0  11984  blres  12220  metrest  12292  elcncf1di  12332