Theorem an32 658

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 656	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2	1	biancomi 467	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 401

This theorem is referenced by:  an32s  664  3anan32OLD  1114  an42ds  1520  inrab2  4270  reupick  4282  difxp  6161  imadif  6620  respreima  7061  dff1o6  7273  dfoprab2  7468  f11o  7940  xpassen  9055  dfac5lem1  10103  kmlem3  10132  qbtwnre  13220  elioomnf  13466  modfsummod  15842  pcqcl  16911  tosso  18468  subgdmdprd  20101  ssdifidllem  21484  pjfval2  21859  opsrtoslem1  22206  fvmptnn04if  23006  cmpcov2  23547  tx1cn  23766  tgphaus  24274  isms2  24607  elcncf1di  25054  elii1  25094  isclmp  25256  bddiblnc  26001  dvreslem  26068  dvdsflsumcom  27352  upgr2wlk  30016  upgrtrls  30049  upgristrl  30050  fusgr2wsp2nb  30685  cvnbtwn3  32640  an52ds  32802  an62ds  32803  an72ds  32804  an82ds  32805  fdifsupp  33030  ssmxidllem  33756  ordtconnlem1  34314  1stmbfm  34650  eulerpartlemn  34771  ballotlem2  34879  reprinrn  35005  reprdifc  35014  cusgr3cyclex  35628  dfon3  36382  lemsuccf  36431  brsegle2  36601  bj-restn0b  37733  bj-opelidb1  37797  matunitlindflem2  38268  poimirlem25  38296  ftc1anc  38352  disjlem17  39551  prtlem17  39650  lcvnbtwn3  39802  cvrnbtwn3  40050  islpln5  40309  islvol5  40353  lhpexle3  40786  dibelval3  41921  dihglb2  42116  pm11.6  45102  stoweidlem17  46731  smfsuplem1  47525