Theorem an32 642

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 640	. 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  648  3anan32  1095  indifdirOLD  4216  inrab2  4238  reupick  4249  difxp  6056  imadif  6502  respreima  6925  dff1o6  7128  dfoprab2  7311  f11o  7763  xpassen  8806  dfac5lem1  9810  kmlem3  9839  qbtwnre  12862  elioomnf  13105  modfsummod  15434  pcqcl  16485  tosso  18052  subgdmdprd  19552  pjfval2  20826  opsrtoslem1  21172  fvmptnn04if  21906  cmpcov2  22449  tx1cn  22668  tgphaus  23176  isms2  23511  elcncf1di  23964  elii1  24004  isclmp  24166  bddiblnc  24911  dvreslem  24978  dvdsflsumcom  26242  upgr2wlk  27938  upgrtrls  27971  upgristrl  27972  fusgr2wsp2nb  28599  cvnbtwn3  30551  ssmxidllem  31543  ordtconnlem1  31776  1stmbfm  32127  eulerpartlemn  32248  ballotlem2  32355  reprinrn  32498  reprdifc  32507  cusgr3cyclex  32998  dfon3  34121  brsuccf  34170  brsegle2  34338  bj-restn0b  35189  bj-opelidb1  35251  matunitlindflem2  35701  poimirlem25  35729  ftc1anc  35785  prtlem17  36817  lcvnbtwn3  36969  cvrnbtwn3  37217  islpln5  37476  islvol5  37520  lhpexle3  37953  dibelval3  39088  dihglb2  39283  pm11.6  41899  stoweidlem17  43448  smfsuplem1  44231