Theorem anass 401

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

Syntax hints:   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bianass  469  mpan10  474  an12  561  an32  562  an13  563  an31  564  an4  586  3anass  982  sbidm  1851  4exdistr  1916  2sb5  1983  2sb5rf  1989  sbel2x  1998  r2exf  2495  r19.41  2632  ceqsex3v  2780  ceqsrex2v  2870  rexrab  2901  rexrab2  2905  rexss  3223  inass  3346  difin2  3398  difrab  3410  reupick3  3421  inssdif0im  3491  rexdifpr  3621  rexdifsn  3725  unidif0  4168  bnd2  4174  eqvinop  4244  copsexg  4245  uniuni  4452  rabxp  4664  elvvv  4690  rexiunxp  4770  resopab2  4955  ssrnres  5072  elxp4  5117  elxp5  5118  cnvresima  5119  mptpreima  5123  coass  5148  dff1o2  5467  eqfnfv3  5616  rexsupp  5641  isoini  5819  f1oiso  5827  oprabid  5907  dfoprab2  5922  mpoeq123  5934  mpomptx  5966  resoprab2  5972  ovi3  6011  oprabex3  6130  spc2ed  6234  f1od2  6236  brtpos2  6252  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpassen  6830  ltexpi  7336  enq0enq  7430  enq0tr  7433  prnmaxl  7487  prnminu  7488  genpdflem  7506  ltexprlemm  7599  suplocsrlemb  7805  axaddf  7867  axmulf  7868  rexuz  9580  rexuz2  9581  rexrp  9676  elixx3g  9901  elfz2  10015  fzdifsuc  10081  fzind2  10239  divalgb  11930  gcdass  12016  nnwosdc  12040  lcmass  12085  isprm2  12117  infpn2  12457  issubg3  13052  ntreq0  13635  tx1cn  13772  tx2cn  13773  blres  13937  metrest  14009  elcncf1di  14069  dedekindicclemicc  14113