Theorem an32 659

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  an32s  665  3anan32OLD  1114  an42ds  1519  inrab2  4261  reupick  4273  difxp  6157  imadif  6629  respreima  7070  dff1o6  7287  dfoprab2  7482  f11o  7963  xpassen  9097  dfac5lem1  10209  kmlem3  10238  qbtwnre  13336  elioomnf  13582  modfsummod  15970  pcqcl  17043  tosso  18600  subgdmdprd  20259  ssdifidllem  21649  pjfval2  22024  opsrtoslem1  22373  matunitlindflem2  23004  fvmptnn04if  23176  cmpcov2  23717  tx1cn  23937  tgphaus  24445  isms2  24778  elcncf1di  25225  elii1  25265  isclmp  25427  bddiblnc  26171  dvreslem  26238  dvdsflsumcom  27524  upgr2wlk  30256  upgrtrls  30293  upgristrl  30294  fusgr2wsp2nb  30944  cvnbtwn3  32899  an52ds  33103  an62ds  33104  an72ds  33105  an82ds  33106  fdifsupp  33329  ssmxidllem  34048  ordtconnlem1  34606  1stmbfm  34942  eulerpartlemn  35063  ballotlem2  35171  reprinrn  35297  reprdifc  35306  cusgr3cyclex  35991  dfon3  36750  lemsuccf  36799  brsegle2  36970  bj-restn0b  38120  bj-opelidb1  38183  poimirlem25  38672  ftc1anc  38728  disjlem17  39943  prtlem17  40042  lcvnbtwn3  40194  cvrnbtwn3  40442  islpln5  40701  islvol5  40745  lhpexle3  41178  dibelval3  42313  dihglb2  42508  pm11.6  45485  stoweidlem17  47135  smfsuplem1  47929