Theorem 3anan32 1094

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 1086	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 645	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3ancomb  1096  anandi3r  1100  rabssrabd  4009  dff1o3  6596  bropfvvvvlem  7769  tz7.49c  8065  ispos2  17550  lbsacsbs  19921  obslbs  20419  islbs4  20521  leordtvallem1  21815  trfbas2  22448  isclmp  23702  lssbn  23956  sineq0  25116  dchrelbas3  25822  nb3grpr2  27173  uspgr2wlkeq  27435  2spthd  27727  clwwlknonwwlknonb  27891  frgr2wwlkeu  28112  elicoelioo  30527  cndprobprob  31806  bnj543  32275  cusgr3cyclex  32496  elno3  33275  ellimits  33484  refsymrel2  35963  refsymrel3  35964  dfeqvrel2  35985  dfeqvrel3  35986