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  4267  reupick  4279  difxp  6120  imadif  6574  respreima  7009  dff1o6  7219  dfoprab2  7414  f11o  7889  xpassen  8997  dfac5lem1  10031  kmlem3  10061  qbtwnre  13112  elioomnf  13358  modfsummod  15715  pcqcl  16782  tosso  18338  subgdmdprd  19963  pjfval2  21662  opsrtoslem1  22008  fvmptnn04if  22791  cmpcov2  23332  tx1cn  23551  tgphaus  24059  isms2  24392  elcncf1di  24842  elii1  24885  isclmp  25051  bddiblnc  25797  dvreslem  25864  dvdsflsumcom  27152  upgr2wlk  29689  upgrtrls  29722  upgristrl  29723  fusgr2wsp2nb  30358  cvnbtwn3  32312  an52ds  32474  an62ds  32475  an72ds  32476  an82ds  32477  fdifsupp  32713  ssdifidllem  33486  ssmxidllem  33503  ordtconnlem1  34030  1stmbfm  34366  eulerpartlemn  34487  ballotlem2  34595  reprinrn  34724  reprdifc  34733  cusgr3cyclex  35279  dfon3  36033  lemsuccf  36082  brsegle2  36252  bj-restn0b  37235  bj-opelidb1  37297  matunitlindflem2  37757  poimirlem25  37785  ftc1anc  37841  disjlem17  38997  prtlem17  39075  lcvnbtwn3  39227  cvrnbtwn3  39475  islpln5  39734  islvol5  39778  lhpexle3  40211  dibelval3  41346  dihglb2  41541  pm11.6  44575  stoweidlem17  46203  smfsuplem1  46997