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  an42ds  1491  inrab2  4266  reupick  4278  difxp  6117  imadif  6571  respreima  7005  dff1o6  7215  dfoprab2  7410  f11o  7885  xpassen  8990  dfac5lem1  10020  kmlem3  10050  qbtwnre  13104  elioomnf  13350  modfsummod  15707  pcqcl  16774  tosso  18329  subgdmdprd  19954  pjfval2  21652  opsrtoslem1  21996  fvmptnn04if  22770  cmpcov2  23311  tx1cn  23530  tgphaus  24038  isms2  24371  elcncf1di  24821  elii1  24864  isclmp  25030  bddiblnc  25776  dvreslem  25843  dvdsflsumcom  27131  upgr2wlk  29652  upgrtrls  29685  upgristrl  29686  fusgr2wsp2nb  30321  cvnbtwn3  32275  an52ds  32437  an62ds  32438  an72ds  32439  an82ds  32440  fdifsupp  32673  ssdifidllem  33428  ssmxidllem  33445  ordtconnlem1  33944  1stmbfm  34280  eulerpartlemn  34401  ballotlem2  34509  reprinrn  34638  reprdifc  34647  cusgr3cyclex  35187  dfon3  35941  lemsuccf  35990  brsegle2  36160  bj-restn0b  37142  bj-opelidb1  37204  matunitlindflem2  37663  poimirlem25  37691  ftc1anc  37747  disjlem17  38903  prtlem17  38981  lcvnbtwn3  39133  cvrnbtwn3  39381  islpln5  39640  islvol5  39684  lhpexle3  40117  dibelval3  41252  dihglb2  41447  pm11.6  44490  stoweidlem17  46120  smfsuplem1  46914