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  4322  reupick  4334  difxp  6185  imadif  6651  respreima  7085  dff1o6  7294  dfoprab2  7490  f11o  7969  xpassen  9104  dfac5lem1  10160  kmlem3  10190  qbtwnre  13237  elioomnf  13480  modfsummod  15826  pcqcl  16889  tosso  18476  subgdmdprd  20068  pjfval2  21746  opsrtoslem1  22096  fvmptnn04if  22870  cmpcov2  23413  tx1cn  23632  tgphaus  24140  isms2  24475  elcncf1di  24934  elii1  24977  isclmp  25143  bddiblnc  25891  dvreslem  25958  dvdsflsumcom  27245  upgr2wlk  29700  upgrtrls  29733  upgristrl  29734  fusgr2wsp2nb  30362  cvnbtwn3  32316  an42ds  32478  an52ds  32479  an62ds  32480  an72ds  32481  an82ds  32482  fdifsupp  32699  ssdifidllem  33463  ssmxidllem  33480  ordtconnlem1  33884  1stmbfm  34241  eulerpartlemn  34362  ballotlem2  34469  reprinrn  34611  reprdifc  34620  cusgr3cyclex  35120  dfon3  35873  brsuccf  35922  brsegle2  36090  bj-restn0b  37073  bj-opelidb1  37135  matunitlindflem2  37603  poimirlem25  37631  ftc1anc  37687  disjlem17  38780  prtlem17  38857  lcvnbtwn3  39009  cvrnbtwn3  39257  islpln5  39517  islvol5  39561  lhpexle3  39994  dibelval3  41129  dihglb2  41324  pm11.6  44387  stoweidlem17  45972  smfsuplem1  46766