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  4280  reupick  4292  difxp  6137  imadif  6600  respreima  7038  dff1o6  7250  dfoprab2  7447  f11o  7925  xpassen  9035  dfac5lem1  10076  kmlem3  10106  qbtwnre  13159  elioomnf  13405  modfsummod  15760  pcqcl  16827  tosso  18378  subgdmdprd  19966  pjfval2  21618  opsrtoslem1  21962  fvmptnn04if  22736  cmpcov2  23277  tx1cn  23496  tgphaus  24004  isms2  24338  elcncf1di  24788  elii1  24831  isclmp  24997  bddiblnc  25743  dvreslem  25810  dvdsflsumcom  27098  upgr2wlk  29596  upgrtrls  29629  upgristrl  29630  fusgr2wsp2nb  30263  cvnbtwn3  32217  an42ds  32379  an52ds  32380  an62ds  32381  an72ds  32382  an82ds  32383  fdifsupp  32608  ssdifidllem  33427  ssmxidllem  33444  ordtconnlem1  33914  1stmbfm  34251  eulerpartlemn  34372  ballotlem2  34480  reprinrn  34609  reprdifc  34618  cusgr3cyclex  35123  dfon3  35880  brsuccf  35929  brsegle2  36097  bj-restn0b  37079  bj-opelidb1  37141  matunitlindflem2  37611  poimirlem25  37639  ftc1anc  37695  disjlem17  38791  prtlem17  38869  lcvnbtwn3  39021  cvrnbtwn3  39269  islpln5  39529  islvol5  39573  lhpexle3  40006  dibelval3  41141  dihglb2  41336  pm11.6  44381  stoweidlem17  46015  smfsuplem1  46809