Theorem an32 834

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		anass 678	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 833	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3		ancom 464	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
4	1, 2, 3	3bitri 284	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 194   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  an32s  841  3anan32  1042  indifdir  3841  inrab2  3858  reupick  3869  difxp  5462  resco  5541  imadif  5872  respreima  6236  dff1o6  6408  dfoprab2  6576  f11o  6998  mpt2curryd  7259  xpassen  7916  dfac5lem1  8806  kmlem3  8834  qbtwnre  11865  elioomnf  12097  modfsummod  14315  pcqcl  15347  tosso  16807  subgdmdprd  18204  opsrtoslem1  19253  pjfval2  19819  fvmptnn04if  20420  cmpcov2  20950  tx1cn  21169  tgphaus  21677  isms2  22012  elcncf1di  22453  elii1  22489  isclmp  22652  dvreslem  23423  dvdsflsumcom  24658  is2wlk  25888  cvnbtwn3  28324  ordtconlem1  29091  1stmbfm  29442  eulerpartlemn  29563  ballotlem2  29670  dfon3  30962  brsuccf  31011  brsegle2  31179  bj-restn0b  32008  matunitlindflem2  32359  poimirlem25  32387  bddiblnc  32433  ftc1anc  32446  prtlem17  32962  lcvnbtwn3  33116  cvrnbtwn3  33364  islpln5  33622  islvol5  33666  lhpexle3  34099  dibelval3  35237  dihglb2  35432  pm11.6  37397  stoweidlem17  38693  upgr2wlk  40857  upgrtrls  40890  upgristrl  40891