Theorem 3anan32 1082

Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Assertion

Ref	Expression
3anan32	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Proof of Theorem 3anan32

Step	Hyp	Ref	Expression
1		df-3an 1073	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 625	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 264	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 382   ∧ w3a 1071

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 383  df-3an 1073

This theorem is referenced by:  3ancomb  1085  anandi3r  1092  rabssrabd  3838  dff1o3  6285  bropfvvvvlem  7411  tz7.49c  7698  ispos2  17156  lbsacsbs  19371  obslbs  20291  islbs4  20388  leordtvallem1  21235  trfbas2  21867  isclmp  23116  lssbn  23367  sineq0  24494  dchrelbas3  25184  nb3grpr2  26508  uspgr2wlkeq  26777  2spthd  27088  clwwlknonwwlknonb  27281  clwwlknonwwlknonbOLD  27282  frgr2wwlkeu  27509  elicoelioo  29880  cndprobprob  30840  bnj543  31301  elno3  32145  ellimits  32354  refsymrel2  34655  refsymrel3  34656