Theorem 3anan32 1081

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 636	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 267	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 386   ∧ 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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3ancomb  1084  anandi3r  1091  rabssrabd  3910  dff1o3  6399  bropfvvvvlem  7539  tz7.49c  7826  ispos2  17338  lbsacsbs  19557  obslbs  20477  islbs4  20579  leordtvallem1  21426  trfbas2  22059  isclmp  23308  lssbn  23562  sineq0  24715  dchrelbas3  25419  nb3grpr2  26735  uspgr2wlkeq  26997  2spthd  27325  clwwlknonwwlknonb  27512  frgr2wwlkeu  27739  elicoelioo  30108  cndprobprob  31103  bnj543  31566  elno3  32401  ellimits  32610  refsymrel2  34946  refsymrel3  34947  dfeqvrel2  34967  dfeqvrel3  34968