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 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  652  3anan32  1098  indifdirOLD  4174  inrab2  4194  reupick  4205  difxp  5990  imadif  6417  respreima  6837  dff1o6  7037  dfoprab2  7220  f11o  7666  xpassen  8653  dfac5lem1  9616  kmlem3  9645  qbtwnre  12668  elioomnf  12911  modfsummod  15235  pcqcl  16286  tosso  17755  subgdmdprd  19268  pjfval2  20518  opsrtoslem1  20859  fvmptnn04if  21593  cmpcov2  22134  tx1cn  22353  tgphaus  22861  isms2  23196  elcncf1di  23640  elii1  23680  isclmp  23842  bddiblnc  24586  dvreslem  24653  dvdsflsumcom  25917  upgr2wlk  27602  upgrtrls  27635  upgristrl  27636  fusgr2wsp2nb  28263  cvnbtwn3  30215  ssmxidllem  31205  ordtconnlem1  31438  1stmbfm  31789  eulerpartlemn  31910  ballotlem2  32017  reprinrn  32160  reprdifc  32169  cusgr3cyclex  32661  dfon3  33824  brsuccf  33873  brsegle2  34041  bj-restn0b  34872  bj-opelidb1  34934  matunitlindflem2  35386  poimirlem25  35414  ftc1anc  35470  prtlem17  36502  lcvnbtwn3  36654  cvrnbtwn3  36902  islpln5  37161  islvol5  37205  lhpexle3  37638  dibelval3  38773  dihglb2  38968  pm11.6  41532  stoweidlem17  43084  smfsuplem1  43867