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  1520  inrab2  4265  reupick  4277  difxp  6173  imadif  6654  respreima  7097  dff1o6  7314  dfoprab2  7509  f11o  7993  xpassen  9128  dfac5lem1  10241  kmlem3  10270  qbtwnre  13369  elioomnf  13615  modfsummod  16005  pcqcl  17078  tosso  18641  subgdmdprd  20301  ssdifidllem  21691  pjfval2  22070  opsrtoslem1  22419  matunitlindflem2  23050  fvmptnn04if  23222  cmpcov2  23763  tx1cn  23983  tgphaus  24491  isms2  24824  elcncf1di  25271  elii1  25311  isclmp  25473  bddiblnc  26217  dvreslem  26284  dvdsflsumcom  27572  upgr2wlk  30304  upgrtrls  30341  upgristrl  30342  fusgr2wsp2nb  30992  cvnbtwn3  32947  an52ds  33151  an62ds  33152  an72ds  33153  an82ds  33154  fdifsupp  33375  ssmxidllem  34102  ordtconnlem1  34667  1stmbfm  35003  eulerpartlemn  35124  ballotlem2  35232  reprinrn  35358  reprdifc  35367  cusgr3cyclex  36109  dfon3  36869  lemsuccf  36918  brsegle2  37089  bj-restn0b  38282  bj-opelidb1  38342  poimirlem25  38831  ftc1anc  38887  disjlem17  40100  prtlem17  40199  lcvnbtwn3  40351  cvrnbtwn3  40599  islpln5  40858  islvol5  40902  lhpexle3  41335  dibelval3  42470  dihglb2  42665  pm11.6  45637  stoweidlem17  47300  smfsuplem1  48094