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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  an32s  651  3anan32  1098  indifdirOLD  4285  inrab2  4307  reupick  4318  difxp  6161  imadif  6630  respreima  7065  dff1o6  7270  dfoprab2  7464  f11o  7930  xpassen  9063  dfac5lem1  10115  kmlem3  10144  qbtwnre  13175  elioomnf  13418  modfsummod  15737  pcqcl  16786  tosso  18369  subgdmdprd  19899  pjfval2  21256  opsrtoslem1  21608  fvmptnn04if  22343  cmpcov2  22886  tx1cn  23105  tgphaus  23613  isms2  23948  elcncf1di  24403  elii1  24443  isclmp  24605  bddiblnc  25351  dvreslem  25418  dvdsflsumcom  26682  upgr2wlk  28915  upgrtrls  28948  upgristrl  28949  fusgr2wsp2nb  29577  cvnbtwn3  31529  ssmxidllem  32578  ordtconnlem1  32893  1stmbfm  33248  eulerpartlemn  33369  ballotlem2  33476  reprinrn  33619  reprdifc  33628  cusgr3cyclex  34116  dfon3  34853  brsuccf  34902  brsegle2  35070  bj-restn0b  35961  bj-opelidb1  36023  matunitlindflem2  36474  poimirlem25  36502  ftc1anc  36558  disjlem17  37658  prtlem17  37735  lcvnbtwn3  37887  cvrnbtwn3  38135  islpln5  38395  islvol5  38439  lhpexle3  38872  dibelval3  40007  dihglb2  40202  pm11.6  43137  stoweidlem17  44720  smfsuplem1  45514