Theorem an32 645

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 643	. 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  651  3anan32  1097  inrab2  4336  reupick  4348  difxp  6195  imadif  6662  respreima  7099  dff1o6  7311  dfoprab2  7508  f11o  7987  xpassen  9132  dfac5lem1  10192  kmlem3  10222  qbtwnre  13261  elioomnf  13504  modfsummod  15842  pcqcl  16903  tosso  18489  subgdmdprd  20078  pjfval2  21752  opsrtoslem1  22102  fvmptnn04if  22876  cmpcov2  23419  tx1cn  23638  tgphaus  24146  isms2  24481  elcncf1di  24940  elii1  24983  isclmp  25149  bddiblnc  25897  dvreslem  25964  dvdsflsumcom  27249  upgr2wlk  29704  upgrtrls  29737  upgristrl  29738  fusgr2wsp2nb  30366  cvnbtwn3  32320  an42ds  32479  an52ds  32480  an62ds  32481  an72ds  32482  an82ds  32483  ssdifidllem  33449  ssmxidllem  33466  ordtconnlem1  33870  1stmbfm  34225  eulerpartlemn  34346  ballotlem2  34453  reprinrn  34595  reprdifc  34604  cusgr3cyclex  35104  dfon3  35856  brsuccf  35905  brsegle2  36073  bj-restn0b  37057  bj-opelidb1  37119  matunitlindflem2  37577  poimirlem25  37605  ftc1anc  37661  disjlem17  38755  prtlem17  38832  lcvnbtwn3  38984  cvrnbtwn3  39232  islpln5  39492  islvol5  39536  lhpexle3  39969  dibelval3  41104  dihglb2  41299  pm11.6  44361  stoweidlem17  45938  smfsuplem1  46732