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  4263  reupick  4275  difxp  6156  imadif  6617  respreima  7058  dff1o6  7276  dfoprab2  7471  f11o  7944  xpassen  9069  dfac5lem1  10126  kmlem3  10155  qbtwnre  13251  elioomnf  13497  modfsummod  15881  pcqcl  16948  tosso  18505  subgdmdprd  20163  ssdifidllem  21547  pjfval2  21922  opsrtoslem1  22271  matunitlindflem2  22902  fvmptnn04if  23074  cmpcov2  23615  tx1cn  23835  tgphaus  24343  isms2  24676  elcncf1di  25123  elii1  25163  isclmp  25325  bddiblnc  26069  dvreslem  26136  dvdsflsumcom  27424  upgr2wlk  30126  upgrtrls  30163  upgristrl  30164  fusgr2wsp2nb  30814  cvnbtwn3  32769  an52ds  32931  an62ds  32932  an72ds  32933  an82ds  32934  fdifsupp  33157  ssmxidllem  33876  ordtconnlem1  34434  1stmbfm  34771  eulerpartlemn  34892  ballotlem2  35000  reprinrn  35126  reprdifc  35135  cusgr3cyclex  35725  dfon3  36469  lemsuccf  36518  brsegle2  36689  bj-restn0b  37841  bj-opelidb1  37905  poimirlem25  38394  ftc1anc  38450  disjlem17  39650  prtlem17  39749  lcvnbtwn3  39901  cvrnbtwn3  40149  islpln5  40408  islvol5  40452  lhpexle3  40885  dibelval3  42020  dihglb2  42215  pm11.6  45216  stoweidlem17  46845  smfsuplem1  47639