Theorem 3anan32 1097

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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 647	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3ancomb  1099  anandi3r  1103  rabssrabd  4024  dff1o3  6781  bropfvvvvlem  8035  tz7.49c  8379  ispos2  18275  lbsacsbs  21149  obslbs  21723  islbs4  21825  leordtvallem1  23188  trfbas2  23821  isclmp  25077  lssbn  25332  sineq0  26504  dchrelbas3  27218  elno3  27636  nb3grpr2  29469  uspgr2wlkeq  29732  2spthd  30027  clwwlknonwwlknonb  30194  frgr2wwlkeu  30415  elicoelioo  32869  cndprobprob  34601  bnj543  35054  cusgr3cyclex  35337  ellimits  36109  eldmxrncnvepres  38772  eldmxrncnvepres2  38773  refsymrel2  38989  refsymrel3  38990  dfeqvrel2  39012  dfeqvrel3  39013  i0oii  49410