Theorem an32 646

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 644	. 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  652  3anan32  1096  inrab2  4276  reupick  4288  difxp  6125  imadif  6584  respreima  7020  dff1o6  7232  dfoprab2  7427  f11o  7905  xpassen  9012  dfac5lem1  10052  kmlem3  10082  qbtwnre  13135  elioomnf  13381  modfsummod  15736  pcqcl  16803  tosso  18354  subgdmdprd  19942  pjfval2  21594  opsrtoslem1  21938  fvmptnn04if  22712  cmpcov2  23253  tx1cn  23472  tgphaus  23980  isms2  24314  elcncf1di  24764  elii1  24807  isclmp  24973  bddiblnc  25719  dvreslem  25786  dvdsflsumcom  27074  upgr2wlk  29570  upgrtrls  29603  upgristrl  29604  fusgr2wsp2nb  30236  cvnbtwn3  32190  an42ds  32352  an52ds  32353  an62ds  32354  an72ds  32355  an82ds  32356  fdifsupp  32581  ssdifidllem  33400  ssmxidllem  33417  ordtconnlem1  33887  1stmbfm  34224  eulerpartlemn  34345  ballotlem2  34453  reprinrn  34582  reprdifc  34591  cusgr3cyclex  35096  dfon3  35853  brsuccf  35902  brsegle2  36070  bj-restn0b  37052  bj-opelidb1  37114  matunitlindflem2  37584  poimirlem25  37612  ftc1anc  37668  disjlem17  38764  prtlem17  38842  lcvnbtwn3  38994  cvrnbtwn3  39242  islpln5  39502  islvol5  39546  lhpexle3  39979  dibelval3  41114  dihglb2  41309  pm11.6  44354  stoweidlem17  45988  smfsuplem1  46782