Theorem an32 659

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an32s  665  3anan32OLD  1114  an42ds  1520  inrab2  4263  reupick  4275  difxp  6155  imadif  6622  respreima  7063  dff1o6  7281  dfoprab2  7476  f11o  7957  xpassen  9083  dfac5lem1  10195  kmlem3  10224  qbtwnre  13322  elioomnf  13568  modfsummod  15954  pcqcl  17027  tosso  18584  subgdmdprd  20243  ssdifidllem  21633  pjfval2  22008  opsrtoslem1  22357  matunitlindflem2  22988  fvmptnn04if  23160  cmpcov2  23701  tx1cn  23921  tgphaus  24429  isms2  24762  elcncf1di  25209  elii1  25249  isclmp  25411  bddiblnc  26155  dvreslem  26222  dvdsflsumcom  27508  upgr2wlk  30240  upgrtrls  30277  upgristrl  30278  fusgr2wsp2nb  30928  cvnbtwn3  32883  an52ds  33045  an62ds  33046  an72ds  33047  an82ds  33048  fdifsupp  33271  ssmxidllem  33991  ordtconnlem1  34549  1stmbfm  34885  eulerpartlemn  35006  ballotlem2  35114  reprinrn  35240  reprdifc  35249  cusgr3cyclex  35890  dfon3  36634  lemsuccf  36683  brsegle2  36854  bj-restn0b  37992  bj-opelidb1  38054  poimirlem25  38543  ftc1anc  38599  disjlem17  39814  prtlem17  39913  lcvnbtwn3  40065  cvrnbtwn3  40313  islpln5  40572  islvol5  40616  lhpexle3  41049  dibelval3  42184  dihglb2  42379  pm11.6  45361  stoweidlem17  46996  smfsuplem1  47790