Theorem an32 646

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 644	. 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  652  3anan32  1096  inrab2  4292  reupick  4304  difxp  6153  imadif  6620  respreima  7056  dff1o6  7268  dfoprab2  7465  f11o  7945  xpassen  9080  dfac5lem1  10137  kmlem3  10167  qbtwnre  13215  elioomnf  13461  modfsummod  15810  pcqcl  16876  tosso  18429  subgdmdprd  20017  pjfval2  21669  opsrtoslem1  22013  fvmptnn04if  22787  cmpcov2  23328  tx1cn  23547  tgphaus  24055  isms2  24389  elcncf1di  24839  elii1  24882  isclmp  25048  bddiblnc  25795  dvreslem  25862  dvdsflsumcom  27150  upgr2wlk  29648  upgrtrls  29681  upgristrl  29682  fusgr2wsp2nb  30315  cvnbtwn3  32269  an42ds  32431  an52ds  32432  an62ds  32433  an72ds  32434  an82ds  32435  fdifsupp  32662  ssdifidllem  33471  ssmxidllem  33488  ordtconnlem1  33955  1stmbfm  34292  eulerpartlemn  34413  ballotlem2  34521  reprinrn  34650  reprdifc  34659  cusgr3cyclex  35158  dfon3  35910  brsuccf  35959  brsegle2  36127  bj-restn0b  37109  bj-opelidb1  37171  matunitlindflem2  37641  poimirlem25  37669  ftc1anc  37725  disjlem17  38817  prtlem17  38894  lcvnbtwn3  39046  cvrnbtwn3  39294  islpln5  39554  islvol5  39598  lhpexle3  40031  dibelval3  41166  dihglb2  41361  pm11.6  44416  stoweidlem17  46046  smfsuplem1  46840