Theorem an32 839

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		anass 681	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 838	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3		ancom 466	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
4	1, 2, 3	3bitri 286	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  an32s  846  3anan32  1050  indifdir  3883  inrab2  3900  reupick  3911  difxp  5558  resco  5639  imadif  5973  respreima  6344  dff1o6  6531  dfoprab2  6701  f11o  7128  mpt2curryd  7395  xpassen  8054  dfac5lem1  8946  kmlem3  8974  qbtwnre  12030  elioomnf  12268  modfsummod  14526  pcqcl  15561  tosso  17036  subgdmdprd  18433  opsrtoslem1  19484  pjfval2  20053  fvmptnn04if  20654  cmpcov2  21193  tx1cn  21412  tgphaus  21920  isms2  22255  elcncf1di  22698  elii1  22734  isclmp  22897  dvreslem  23673  dvdsflsumcom  24914  upgr2wlk  26564  upgrtrls  26598  upgristrl  26599  fusgr2wsp2nb  27198  cvnbtwn3  29147  ordtconnlem1  29970  1stmbfm  30322  eulerpartlemn  30443  ballotlem2  30550  reprinrn  30696  reprdifc  30705  dfon3  31999  brsuccf  32048  brsegle2  32216  bj-restn0b  33044  matunitlindflem2  33406  poimirlem25  33434  bddiblnc  33480  ftc1anc  33493  prtlem17  34161  lcvnbtwn3  34315  cvrnbtwn3  34563  islpln5  34821  islvol5  34865  lhpexle3  35298  dibelval3  36436  dihglb2  36631  pm11.6  38592  stoweidlem17  40234  smfsuplem1  41017