Theorem anass 399

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

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpan10  466  an12  551  an32  552  an13  553  an31  554  an4  576  3anass  967  sbidm  1824  4exdistr  1889  2sb5  1959  2sb5rf  1965  sbel2x  1974  r2exf  2456  r19.41  2589  ceqsex3v  2731  ceqsrex2v  2821  rexrab  2851  rexrab2  2855  rexss  3169  inass  3291  difin2  3343  difrab  3355  reupick3  3366  inssdif0im  3435  rexdifpr  3560  rexdifsn  3663  unidif0  4099  bnd2  4105  eqvinop  4173  copsexg  4174  uniuni  4380  rabxp  4584  elvvv  4610  rexiunxp  4689  resopab2  4874  ssrnres  4989  elxp4  5034  elxp5  5035  cnvresima  5036  mptpreima  5040  coass  5065  dff1o2  5380  eqfnfv3  5528  rexsupp  5552  isoini  5727  f1oiso  5735  oprabid  5811  dfoprab2  5826  mpoeq123  5838  mpomptx  5870  resoprab2  5876  ovi3  5915  oprabex3  6035  spc2ed  6138  f1od2  6140  brtpos2  6156  mapsnen  6713  xpsnen  6723  xpcomco  6728  xpassen  6732  ltexpi  7169  enq0enq  7263  enq0tr  7266  prnmaxl  7320  prnminu  7321  genpdflem  7339  ltexprlemm  7432  suplocsrlemb  7638  axaddf  7700  axmulf  7701  rexuz  9402  rexuz2  9403  rexrp  9493  elixx3g  9714  elfz2  9828  fzdifsuc  9892  fzind2  10047  divalgb  11658  gcdass  11739  lcmass  11802  isprm2  11834  ntreq0  12340  tx1cn  12477  tx2cn  12478  blres  12642  metrest  12714  elcncf1di  12774  dedekindicclemicc  12818