Theorem an32 652

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 650	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2	1	biancomi 463	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  an32s  658  3anan32  1102  an42ds  1497  inrab2  4245  reupick  4257  difxp  6115  imadif  6569  respreima  7007  dff1o6  7219  dfoprab2  7414  f11o  7889  xpassen  8999  dfac5lem1  10036  kmlem3  10066  qbtwnre  13142  elioomnf  13388  modfsummod  15748  pcqcl  16818  tosso  18374  subgdmdprd  20002  pjfval2  21684  opsrtoslem1  22031  fvmptnn04if  22832  cmpcov2  23373  tx1cn  23592  tgphaus  24100  isms2  24433  elcncf1di  24880  elii1  24920  isclmp  25082  bddiblnc  25827  dvreslem  25894  dvdsflsumcom  27169  upgr2wlk  29753  upgrtrls  29786  upgristrl  29787  fusgr2wsp2nb  30422  cvnbtwn3  32377  an52ds  32539  an62ds  32540  an72ds  32541  an82ds  32542  fdifsupp  32777  ssdifidllem  33539  ssmxidllem  33556  ordtconnlem1  34108  1stmbfm  34444  eulerpartlemn  34565  ballotlem2  34673  reprinrn  34802  reprdifc  34811  cusgr3cyclex  35364  dfon3  36118  lemsuccf  36167  brsegle2  36337  bj-restn0b  37449  bj-opelidb1  37513  matunitlindflem2  37984  poimirlem25  38012  ftc1anc  38068  disjlem17  39269  prtlem17  39368  lcvnbtwn3  39520  cvrnbtwn3  39768  islpln5  40027  islvol5  40071  lhpexle3  40504  dibelval3  41639  dihglb2  41834  pm11.6  44836  stoweidlem17  46460  smfsuplem1  47254