Theorem an32 643

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  an32s  649  3anan32  1096  indifdirOLD  4220  inrab2  4242  reupick  4253  difxp  6072  imadif  6525  respreima  6952  dff1o6  7156  dfoprab2  7342  f11o  7798  xpassen  8862  dfac5lem1  9888  kmlem3  9917  qbtwnre  12942  elioomnf  13185  modfsummod  15515  pcqcl  16566  tosso  18146  subgdmdprd  19646  pjfval2  20925  opsrtoslem1  21271  fvmptnn04if  22007  cmpcov2  22550  tx1cn  22769  tgphaus  23277  isms2  23612  elcncf1di  24067  elii1  24107  isclmp  24269  bddiblnc  25015  dvreslem  25082  dvdsflsumcom  26346  upgr2wlk  28045  upgrtrls  28078  upgristrl  28079  fusgr2wsp2nb  28707  cvnbtwn3  30659  ssmxidllem  31650  ordtconnlem1  31883  1stmbfm  32236  eulerpartlemn  32357  ballotlem2  32464  reprinrn  32607  reprdifc  32616  cusgr3cyclex  33107  dfon3  34203  brsuccf  34252  brsegle2  34420  bj-restn0b  35271  bj-opelidb1  35333  matunitlindflem2  35783  poimirlem25  35811  ftc1anc  35867  prtlem17  36897  lcvnbtwn3  37049  cvrnbtwn3  37297  islpln5  37556  islvol5  37600  lhpexle3  38033  dibelval3  39168  dihglb2  39363  pm11.6  42017  stoweidlem17  43565  smfsuplem1  44355