Theorem an32 658

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  an32s  664  3anan32OLD  1112  an42ds  1517  inrab2  4278  reupick  4290  difxp  6162  imadif  6621  respreima  7062  dff1o6  7274  dfoprab2  7469  f11o  7943  xpassen  9058  dfac5lem1  10106  kmlem3  10135  qbtwnre  13224  elioomnf  13470  modfsummod  15845  pcqcl  16915  tosso  18472  subgdmdprd  20105  ssdifidllem  21452  pjfval2  21827  opsrtoslem1  22174  fvmptnn04if  22974  cmpcov2  23515  tx1cn  23734  tgphaus  24242  isms2  24575  elcncf1di  25022  elii1  25062  isclmp  25224  bddiblnc  25969  dvreslem  26036  dvdsflsumcom  27317  upgr2wlk  29956  upgrtrls  29989  upgristrl  29990  fusgr2wsp2nb  30625  cvnbtwn3  32580  an52ds  32742  an62ds  32743  an72ds  32744  an82ds  32745  fdifsupp  32970  ssmxidllem  33700  ordtconnlem1  34258  1stmbfm  34594  eulerpartlemn  34715  ballotlem2  34823  reprinrn  34949  reprdifc  34958  cusgr3cyclex  35526  dfon3  36280  lemsuccf  36329  brsegle2  36499  bj-restn0b  37620  bj-opelidb1  37684  matunitlindflem2  38155  poimirlem25  38183  ftc1anc  38239  disjlem17  39440  prtlem17  39539  lcvnbtwn3  39691  cvrnbtwn3  39939  islpln5  40198  islvol5  40242  lhpexle3  40675  dibelval3  41810  dihglb2  42005  pm11.6  44993  stoweidlem17  46622  smfsuplem1  47416