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 466	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  an32s  651  3anan32  1094  indifdir  4210  inrab2  4228  reupick  4239  difxp  5988  imadif  6408  respreima  6813  dff1o6  7010  dfoprab2  7191  f11o  7630  xpassen  8594  dfac5lem1  9534  kmlem3  9563  qbtwnre  12580  elioomnf  12822  modfsummod  15141  pcqcl  16183  tosso  17638  subgdmdprd  19149  pjfval2  20398  opsrtoslem1  20723  fvmptnn04if  21454  cmpcov2  21995  tx1cn  22214  tgphaus  22722  isms2  23057  elcncf1di  23500  elii1  23540  isclmp  23702  bddiblnc  24445  dvreslem  24512  dvdsflsumcom  25773  upgr2wlk  27458  upgrtrls  27491  upgristrl  27492  fusgr2wsp2nb  28119  cvnbtwn3  30071  ssmxidllem  31049  ordtconnlem1  31277  1stmbfm  31628  eulerpartlemn  31749  ballotlem2  31856  reprinrn  31999  reprdifc  32008  cusgr3cyclex  32496  dfon3  33466  brsuccf  33515  brsegle2  33683  bj-restn0b  34506  bj-opelidb1  34568  matunitlindflem2  35054  poimirlem25  35082  ftc1anc  35138  prtlem17  36172  lcvnbtwn3  36324  cvrnbtwn3  36572  islpln5  36831  islvol5  36875  lhpexle3  37308  dibelval3  38443  dihglb2  38638  pm11.6  41096  stoweidlem17  42659  smfsuplem1  43442