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  4262  reupick  4274  difxp  6106  imadif  6560  respreima  6994  dff1o6  7204  dfoprab2  7399  f11o  7874  xpassen  8979  dfac5lem1  10009  kmlem3  10039  qbtwnre  13093  elioomnf  13339  modfsummod  15696  pcqcl  16763  tosso  18318  subgdmdprd  19943  pjfval2  21641  opsrtoslem1  21985  fvmptnn04if  22759  cmpcov2  23300  tx1cn  23519  tgphaus  24027  isms2  24360  elcncf1di  24810  elii1  24853  isclmp  25019  bddiblnc  25765  dvreslem  25832  dvdsflsumcom  27120  upgr2wlk  29640  upgrtrls  29673  upgristrl  29674  fusgr2wsp2nb  30306  cvnbtwn3  32260  an52ds  32422  an62ds  32423  an72ds  32424  an82ds  32425  fdifsupp  32658  ssdifidllem  33413  ssmxidllem  33430  ordtconnlem1  33929  1stmbfm  34265  eulerpartlemn  34386  ballotlem2  34494  reprinrn  34623  reprdifc  34632  cusgr3cyclex  35172  dfon3  35926  brsuccf  35975  brsegle2  36143  bj-restn0b  37125  bj-opelidb1  37187  matunitlindflem2  37657  poimirlem25  37685  ftc1anc  37741  disjlem17  38837  prtlem17  38915  lcvnbtwn3  39067  cvrnbtwn3  39315  islpln5  39574  islvol5  39618  lhpexle3  40051  dibelval3  41186  dihglb2  41381  pm11.6  44425  stoweidlem17  46055  smfsuplem1  46849