Theorem an32 856

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 682	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12 855	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3		ancom 465	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
4	1, 2, 3	3bitri 286	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  an32s  863  3anan32  1068  indifdir  3916  inrab2  3933  reupick  3944  difxp  5593  resco  5677  imadif  6011  respreima  6384  dff1o6  6571  dfoprab2  6743  f11o  7170  mpt2curryd  7440  xpassen  8095  dfac5lem1  8984  kmlem3  9012  qbtwnre  12068  elioomnf  12306  modfsummod  14570  pcqcl  15608  tosso  17083  subgdmdprd  18479  opsrtoslem1  19532  pjfval2  20101  fvmptnn04if  20702  cmpcov2  21241  tx1cn  21460  tgphaus  21967  isms2  22302  elcncf1di  22745  elii1  22781  isclmp  22943  dvreslem  23718  dvdsflsumcom  24959  upgr2wlk  26620  upgrtrls  26654  upgristrl  26655  fusgr2wsp2nb  27314  cvnbtwn3  29275  ordtconnlem1  30098  1stmbfm  30450  eulerpartlemn  30571  ballotlem2  30678  reprinrn  30824  reprdifc  30833  dfon3  32124  brsuccf  32173  brsegle2  32341  bj-restn0b  33169  matunitlindflem2  33536  poimirlem25  33564  bddiblnc  33610  ftc1anc  33623  prtlem17  34480  lcvnbtwn3  34633  cvrnbtwn3  34881  islpln5  35139  islvol5  35183  lhpexle3  35616  dibelval3  36753  dihglb2  36948  pm11.6  38909  stoweidlem17  40552  smfsuplem1  41338