Theorem an32 645

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  an32s  651  3anan32  1095  indifdirOLD  4281  inrab2  4303  reupick  4314  difxp  6162  imadif  6631  respreima  7069  dff1o6  7278  dfoprab2  7472  f11o  7944  xpassen  9084  dfac5lem1  10140  kmlem3  10169  qbtwnre  13204  elioomnf  13447  modfsummod  15766  pcqcl  16818  tosso  18404  subgdmdprd  19984  pjfval2  21636  opsrtoslem1  21992  fvmptnn04if  22744  cmpcov2  23287  tx1cn  23506  tgphaus  24014  isms2  24349  elcncf1di  24808  elii1  24851  isclmp  25017  bddiblnc  25764  dvreslem  25831  dvdsflsumcom  27113  upgr2wlk  29475  upgrtrls  29508  upgristrl  29509  fusgr2wsp2nb  30137  cvnbtwn3  32091  ssmxidllem  33180  ordtconnlem1  33519  1stmbfm  33874  eulerpartlemn  33995  ballotlem2  34102  reprinrn  34244  reprdifc  34253  cusgr3cyclex  34740  dfon3  35482  brsuccf  35531  brsegle2  35699  bj-restn0b  36564  bj-opelidb1  36626  matunitlindflem2  37084  poimirlem25  37112  ftc1anc  37168  disjlem17  38265  prtlem17  38342  lcvnbtwn3  38494  cvrnbtwn3  38742  islpln5  39002  islvol5  39046  lhpexle3  39479  dibelval3  40614  dihglb2  40809  pm11.6  43823  stoweidlem17  45399  smfsuplem1  46193