Theorem 3anan32 1096

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

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

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 1088

This theorem is referenced by:  3ancomb  1098  anandi3r  1102  rabssrabd  4049  dff1o3  6809  bropfvvvvlem  8073  tz7.49c  8417  ispos2  18283  lbsacsbs  21073  obslbs  21646  islbs4  21748  leordtvallem1  23104  trfbas2  23737  isclmp  25004  lssbn  25259  sineq0  26440  dchrelbas3  27156  elno3  27574  nb3grpr2  29317  uspgr2wlkeq  29581  2spthd  29878  clwwlknonwwlknonb  30042  frgr2wwlkeu  30263  elicoelioo  32708  cndprobprob  34436  bnj543  34890  cusgr3cyclex  35130  ellimits  35905  eldmxrncnvepres  38403  eldmxrncnvepres2  38404  refsymrel2  38565  refsymrel3  38566  dfeqvrel2  38588  dfeqvrel3  38589  i0oii  48912