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 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  652  3anan32  1096  inrab2  4283  reupick  4295  difxp  6140  imadif  6603  respreima  7041  dff1o6  7253  dfoprab2  7450  f11o  7928  xpassen  9040  dfac5lem1  10083  kmlem3  10113  qbtwnre  13166  elioomnf  13412  modfsummod  15767  pcqcl  16834  tosso  18385  subgdmdprd  19973  pjfval2  21625  opsrtoslem1  21969  fvmptnn04if  22743  cmpcov2  23284  tx1cn  23503  tgphaus  24011  isms2  24345  elcncf1di  24795  elii1  24838  isclmp  25004  bddiblnc  25750  dvreslem  25817  dvdsflsumcom  27105  upgr2wlk  29603  upgrtrls  29636  upgristrl  29637  fusgr2wsp2nb  30270  cvnbtwn3  32224  an42ds  32386  an52ds  32387  an62ds  32388  an72ds  32389  an82ds  32390  fdifsupp  32615  ssdifidllem  33434  ssmxidllem  33451  ordtconnlem1  33921  1stmbfm  34258  eulerpartlemn  34379  ballotlem2  34487  reprinrn  34616  reprdifc  34625  cusgr3cyclex  35130  dfon3  35887  brsuccf  35936  brsegle2  36104  bj-restn0b  37086  bj-opelidb1  37148  matunitlindflem2  37618  poimirlem25  37646  ftc1anc  37702  disjlem17  38798  prtlem17  38876  lcvnbtwn3  39028  cvrnbtwn3  39276  islpln5  39536  islvol5  39580  lhpexle3  40013  dibelval3  41148  dihglb2  41343  pm11.6  44388  stoweidlem17  46022  smfsuplem1  46816