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  4258  reupick  4270  difxp  6123  imadif  6577  respreima  7013  dff1o6  7224  dfoprab2  7419  f11o  7894  xpassen  9003  dfac5lem1  10039  kmlem3  10069  qbtwnre  13145  elioomnf  13391  modfsummod  15751  pcqcl  16821  tosso  18377  subgdmdprd  20005  pjfval2  21702  opsrtoslem1  22046  fvmptnn04if  22827  cmpcov2  23368  tx1cn  23587  tgphaus  24095  isms2  24428  elcncf1di  24875  elii1  24915  isclmp  25077  bddiblnc  25822  dvreslem  25889  dvdsflsumcom  27168  upgr2wlk  29753  upgrtrls  29786  upgristrl  29787  fusgr2wsp2nb  30422  cvnbtwn3  32377  an52ds  32539  an62ds  32540  an72ds  32541  an82ds  32542  fdifsupp  32776  ssdifidllem  33534  ssmxidllem  33551  ordtconnlem1  34087  1stmbfm  34423  eulerpartlemn  34544  ballotlem2  34652  reprinrn  34781  reprdifc  34790  cusgr3cyclex  35337  dfon3  36091  lemsuccf  36140  brsegle2  36310  bj-restn0b  37422  bj-opelidb1  37486  matunitlindflem2  37955  poimirlem25  37983  ftc1anc  38039  disjlem17  39240  prtlem17  39339  lcvnbtwn3  39491  cvrnbtwn3  39739  islpln5  39998  islvol5  40042  lhpexle3  40475  dibelval3  41610  dihglb2  41805  pm11.6  44840  stoweidlem17  46466  smfsuplem1  47260