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  1097  inrab2  4317  reupick  4329  difxp  6184  imadif  6650  respreima  7086  dff1o6  7295  dfoprab2  7491  f11o  7971  xpassen  9106  dfac5lem1  10163  kmlem3  10193  qbtwnre  13241  elioomnf  13484  modfsummod  15830  pcqcl  16894  tosso  18464  subgdmdprd  20054  pjfval2  21729  opsrtoslem1  22079  fvmptnn04if  22855  cmpcov2  23398  tx1cn  23617  tgphaus  24125  isms2  24460  elcncf1di  24921  elii1  24964  isclmp  25130  bddiblnc  25877  dvreslem  25944  dvdsflsumcom  27231  upgr2wlk  29686  upgrtrls  29719  upgristrl  29720  fusgr2wsp2nb  30353  cvnbtwn3  32307  an42ds  32469  an52ds  32470  an62ds  32471  an72ds  32472  an82ds  32473  fdifsupp  32694  ssdifidllem  33484  ssmxidllem  33501  ordtconnlem1  33923  1stmbfm  34262  eulerpartlemn  34383  ballotlem2  34491  reprinrn  34633  reprdifc  34642  cusgr3cyclex  35141  dfon3  35893  brsuccf  35942  brsegle2  36110  bj-restn0b  37092  bj-opelidb1  37154  matunitlindflem2  37624  poimirlem25  37652  ftc1anc  37708  disjlem17  38800  prtlem17  38877  lcvnbtwn3  39029  cvrnbtwn3  39277  islpln5  39537  islvol5  39581  lhpexle3  40014  dibelval3  41149  dihglb2  41344  pm11.6  44411  stoweidlem17  46032  smfsuplem1  46826