Theorem an32 642

Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)

Assertion

Ref	Expression
an32	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Proof of Theorem an32

Step	Hyp	Ref	Expression
1		an21 640	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2	1	biancomi 461	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  an32s  648  3anan32  1095  indifdirOLD  4286  inrab2  4308  reupick  4319  difxp  6164  imadif  6633  respreima  7068  dff1o6  7277  dfoprab2  7471  f11o  7937  xpassen  9070  dfac5lem1  10122  kmlem3  10151  qbtwnre  13184  elioomnf  13427  modfsummod  15746  pcqcl  16795  tosso  18378  subgdmdprd  19947  pjfval2  21485  opsrtoslem1  21837  fvmptnn04if  22573  cmpcov2  23116  tx1cn  23335  tgphaus  23843  isms2  24178  elcncf1di  24637  elii1  24680  isclmp  24846  bddiblnc  25593  dvreslem  25660  dvdsflsumcom  26926  upgr2wlk  29190  upgrtrls  29223  upgristrl  29224  fusgr2wsp2nb  29852  cvnbtwn3  31806  ssmxidllem  32861  ordtconnlem1  33200  1stmbfm  33555  eulerpartlemn  33676  ballotlem2  33783  reprinrn  33926  reprdifc  33935  cusgr3cyclex  34423  dfon3  35166  brsuccf  35215  brsegle2  35383  bj-restn0b  36277  bj-opelidb1  36339  matunitlindflem2  36790  poimirlem25  36818  ftc1anc  36874  disjlem17  37974  prtlem17  38051  lcvnbtwn3  38203  cvrnbtwn3  38451  islpln5  38711  islvol5  38755  lhpexle3  39188  dibelval3  40323  dihglb2  40518  pm11.6  43455  stoweidlem17  45033  smfsuplem1  45827