Theorem an32 645

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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  an32s  651  3anan32  1095  indifdirOLD  4286  inrab2  4308  reupick  4319  difxp  6168  imadif  6637  respreima  7075  dff1o6  7284  dfoprab2  7478  f11o  7950  xpassen  9090  dfac5lem1  10146  kmlem3  10175  qbtwnre  13210  elioomnf  13453  modfsummod  15772  pcqcl  16824  tosso  18410  subgdmdprd  19990  pjfval2  21642  opsrtoslem1  21998  fvmptnn04if  22750  cmpcov2  23293  tx1cn  23512  tgphaus  24020  isms2  24355  elcncf1di  24814  elii1  24857  isclmp  25023  bddiblnc  25770  dvreslem  25837  dvdsflsumcom  27119  upgr2wlk  29481  upgrtrls  29514  upgristrl  29515  fusgr2wsp2nb  30143  cvnbtwn3  32097  ssmxidllem  33186  ordtconnlem1  33525  1stmbfm  33880  eulerpartlemn  34001  ballotlem2  34108  reprinrn  34250  reprdifc  34259  cusgr3cyclex  34746  dfon3  35488  brsuccf  35537  brsegle2  35705  bj-restn0b  36570  bj-opelidb1  36632  matunitlindflem2  37090  poimirlem25  37118  ftc1anc  37174  disjlem17  38271  prtlem17  38348  lcvnbtwn3  38500  cvrnbtwn3  38748  islpln5  39008  islvol5  39052  lhpexle3  39485  dibelval3  40620  dihglb2  40815  pm11.6  43829  stoweidlem17  45405  smfsuplem1  46199