Theorem an32 647

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 645	. 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  653  3anan32  1097  an42ds  1492  inrab2  4271  reupick  4283  difxp  6130  imadif  6584  respreima  7020  dff1o6  7231  dfoprab2  7426  f11o  7901  xpassen  9011  dfac5lem1  10045  kmlem3  10075  qbtwnre  13126  elioomnf  13372  modfsummod  15729  pcqcl  16796  tosso  18352  subgdmdprd  19977  pjfval2  21676  opsrtoslem1  22022  fvmptnn04if  22805  cmpcov2  23346  tx1cn  23565  tgphaus  24073  isms2  24406  elcncf1di  24856  elii1  24899  isclmp  25065  bddiblnc  25811  dvreslem  25878  dvdsflsumcom  27166  upgr2wlk  29752  upgrtrls  29785  upgristrl  29786  fusgr2wsp2nb  30421  cvnbtwn3  32376  an52ds  32538  an62ds  32539  an72ds  32540  an82ds  32541  fdifsupp  32775  ssdifidllem  33549  ssmxidllem  33566  ordtconnlem1  34102  1stmbfm  34438  eulerpartlemn  34559  ballotlem2  34667  reprinrn  34796  reprdifc  34805  cusgr3cyclex  35352  dfon3  36106  lemsuccf  36155  brsegle2  36325  bj-restn0b  37344  bj-opelidb1  37408  matunitlindflem2  37868  poimirlem25  37896  ftc1anc  37952  disjlem17  39153  prtlem17  39252  lcvnbtwn3  39404  cvrnbtwn3  39652  islpln5  39911  islvol5  39955  lhpexle3  40388  dibelval3  41523  dihglb2  41718  pm11.6  44748  stoweidlem17  46375  smfsuplem1  47169