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  inrab2  4268  reupick  4280  difxp  6113  imadif  6566  respreima  7000  dff1o6  7212  dfoprab2  7407  f11o  7882  xpassen  8988  dfac5lem1  10017  kmlem3  10047  qbtwnre  13101  elioomnf  13347  modfsummod  15701  pcqcl  16768  tosso  18323  subgdmdprd  19915  pjfval2  21616  opsrtoslem1  21960  fvmptnn04if  22734  cmpcov2  23275  tx1cn  23494  tgphaus  24002  isms2  24336  elcncf1di  24786  elii1  24829  isclmp  24995  bddiblnc  25741  dvreslem  25808  dvdsflsumcom  27096  upgr2wlk  29612  upgrtrls  29645  upgristrl  29646  fusgr2wsp2nb  30278  cvnbtwn3  32232  an42ds  32394  an52ds  32395  an62ds  32396  an72ds  32397  an82ds  32398  fdifsupp  32627  ssdifidllem  33393  ssmxidllem  33410  ordtconnlem1  33891  1stmbfm  34228  eulerpartlemn  34349  ballotlem2  34457  reprinrn  34586  reprdifc  34595  cusgr3cyclex  35109  dfon3  35866  brsuccf  35915  brsegle2  36083  bj-restn0b  37065  bj-opelidb1  37127  matunitlindflem2  37597  poimirlem25  37625  ftc1anc  37681  disjlem17  38777  prtlem17  38855  lcvnbtwn3  39007  cvrnbtwn3  39255  islpln5  39514  islvol5  39558  lhpexle3  39991  dibelval3  41126  dihglb2  41321  pm11.6  44365  stoweidlem17  45998  smfsuplem1  46792