Theorem an32 646

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

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

This theorem is referenced by:  an32s  652  3anan32  1096  an42ds  1491  inrab2  4269  reupick  4281  difxp  6122  imadif  6576  respreima  7011  dff1o6  7221  dfoprab2  7416  f11o  7891  xpassen  8999  dfac5lem1  10033  kmlem3  10063  qbtwnre  13114  elioomnf  13360  modfsummod  15717  pcqcl  16784  tosso  18340  subgdmdprd  19965  pjfval2  21664  opsrtoslem1  22010  fvmptnn04if  22793  cmpcov2  23334  tx1cn  23553  tgphaus  24061  isms2  24394  elcncf1di  24844  elii1  24887  isclmp  25053  bddiblnc  25799  dvreslem  25866  dvdsflsumcom  27154  upgr2wlk  29740  upgrtrls  29773  upgristrl  29774  fusgr2wsp2nb  30409  cvnbtwn3  32363  an52ds  32525  an62ds  32526  an72ds  32527  an82ds  32528  fdifsupp  32764  ssdifidllem  33537  ssmxidllem  33554  ordtconnlem1  34081  1stmbfm  34417  eulerpartlemn  34538  ballotlem2  34646  reprinrn  34775  reprdifc  34784  cusgr3cyclex  35330  dfon3  36084  lemsuccf  36133  brsegle2  36303  bj-restn0b  37296  bj-opelidb1  37358  matunitlindflem2  37818  poimirlem25  37846  ftc1anc  37902  disjlem17  39058  prtlem17  39136  lcvnbtwn3  39288  cvrnbtwn3  39536  islpln5  39795  islvol5  39839  lhpexle3  40272  dibelval3  41407  dihglb2  41602  pm11.6  44633  stoweidlem17  46261  smfsuplem1  47055