Theorem an32 656

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  an32s  662  3anan32OLD  1109  an42ds  1510  inrab2  4269  reupick  4281  difxp  6149  imadif  6605  respreima  7047  dff1o6  7259  dfoprab2  7454  f11o  7928  xpassen  9043  dfac5lem1  10079  kmlem3  10109  qbtwnre  13202  elioomnf  13448  modfsummod  15822  pcqcl  16892  tosso  18449  subgdmdprd  20076  pjfval2  21758  opsrtoslem1  22105  fvmptnn04if  22906  cmpcov2  23447  tx1cn  23666  tgphaus  24174  isms2  24507  elcncf1di  24954  elii1  24994  isclmp  25156  bddiblnc  25901  dvreslem  25968  dvdsflsumcom  27249  upgr2wlk  29864  upgrtrls  29897  upgristrl  29898  fusgr2wsp2nb  30533  cvnbtwn3  32488  an52ds  32650  an62ds  32651  an72ds  32652  an82ds  32653  fdifsupp  32884  ssdifidllem  33640  ssmxidllem  33658  ordtconnlem1  34218  1stmbfm  34554  eulerpartlemn  34675  ballotlem2  34783  reprinrn  34909  reprdifc  34918  cusgr3cyclex  35483  dfon3  36237  lemsuccf  36286  brsegle2  36456  bj-restn0b  37578  bj-opelidb1  37642  matunitlindflem2  38113  poimirlem25  38141  ftc1anc  38197  disjlem17  39398  prtlem17  39497  lcvnbtwn3  39649  cvrnbtwn3  39897  islpln5  40156  islvol5  40200  lhpexle3  40633  dibelval3  41768  dihglb2  41963  pm11.6  44965  stoweidlem17  46588  smfsuplem1  47382