Theorem 3anan32 1102

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 1094	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 652	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 276	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3ancomb  1104  anandi3r  1108  rabssrabd  4014  dff1o3  6773  bropfvvvvlem  8030  tz7.49c  8375  ispos2  18272  lbsacsbs  21149  obslbs  21705  islbs4  21807  leordtvallem1  23193  trfbas2  23826  isclmp  25082  lssbn  25337  sineq0  26506  dchrelbas3  27219  elno3  27637  nb3grpr2  29470  uspgr2wlkeq  29732  2spthd  30027  clwwlknonwwlknonb  30194  frgr2wwlkeu  30415  elicoelioo  32870  cndprobprob  34622  bnj543  35075  cusgr3cyclex  35364  ellimits  36136  eldmxrncnvepres  38801  eldmxrncnvepres2  38802  refsymrel2  39018  refsymrel3  39019  dfeqvrel2  39041  dfeqvrel3  39042  i0oii  49410