Theorem an32 659

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an32s  665  3anan32OLD  1114  an42ds  1520  inrab2  4270  reupick  4282  difxp  6163  imadif  6624  respreima  7065  dff1o6  7282  dfoprab2  7477  f11o  7950  xpassen  9066  dfac5lem1  10123  kmlem3  10152  qbtwnre  13241  elioomnf  13487  modfsummod  15869  pcqcl  16938  tosso  18495  subgdmdprd  20150  ssdifidllem  21534  pjfval2  21909  opsrtoslem1  22256  fvmptnn04if  23056  cmpcov2  23597  tx1cn  23817  tgphaus  24325  isms2  24658  elcncf1di  25105  elii1  25145  isclmp  25307  bddiblnc  26052  dvreslem  26119  dvdsflsumcom  27403  upgr2wlk  30074  upgrtrls  30111  upgristrl  30112  fusgr2wsp2nb  30756  cvnbtwn3  32711  an52ds  32873  an62ds  32874  an72ds  32875  an82ds  32876  fdifsupp  33101  ssmxidllem  33820  ordtconnlem1  34378  1stmbfm  34715  eulerpartlemn  34836  ballotlem2  34944  reprinrn  35070  reprdifc  35079  cusgr3cyclex  35669  dfon3  36419  lemsuccf  36468  brsegle2  36638  bj-restn0b  37790  bj-opelidb1  37854  matunitlindflem2  38325  poimirlem25  38353  ftc1anc  38409  disjlem17  39609  prtlem17  39708  lcvnbtwn3  39860  cvrnbtwn3  40108  islpln5  40367  islvol5  40411  lhpexle3  40844  dibelval3  41979  dihglb2  42174  pm11.6  45160  stoweidlem17  46789  smfsuplem1  47583