Theorem an32 647

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 645	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2	1	biancomi 462	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  an32s  653  3anan32  1097  an42ds  1492  inrab2  4257  reupick  4269  difxp  6128  imadif  6582  respreima  7018  dff1o6  7230  dfoprab2  7425  f11o  7900  xpassen  9009  dfac5lem1  10045  kmlem3  10075  qbtwnre  13151  elioomnf  13397  modfsummod  15757  pcqcl  16827  tosso  18383  subgdmdprd  20011  pjfval2  21689  opsrtoslem1  22033  fvmptnn04if  22814  cmpcov2  23355  tx1cn  23574  tgphaus  24082  isms2  24415  elcncf1di  24862  elii1  24902  isclmp  25064  bddiblnc  25809  dvreslem  25876  dvdsflsumcom  27151  upgr2wlk  29735  upgrtrls  29768  upgristrl  29769  fusgr2wsp2nb  30404  cvnbtwn3  32359  an52ds  32521  an62ds  32522  an72ds  32523  an82ds  32524  fdifsupp  32758  ssdifidllem  33516  ssmxidllem  33533  ordtconnlem1  34068  1stmbfm  34404  eulerpartlemn  34525  ballotlem2  34633  reprinrn  34762  reprdifc  34771  cusgr3cyclex  35318  dfon3  36072  lemsuccf  36121  brsegle2  36291  bj-restn0b  37403  bj-opelidb1  37467  matunitlindflem2  37938  poimirlem25  37966  ftc1anc  38022  disjlem17  39223  prtlem17  39322  lcvnbtwn3  39474  cvrnbtwn3  39722  islpln5  39981  islvol5  40025  lhpexle3  40458  dibelval3  41593  dihglb2  41788  pm11.6  44819  stoweidlem17  46445  smfsuplem1  47239