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  4063  dff1o3  6829  bropfvvvvlem  8095  tz7.49c  8465  ispos2  18332  lbsacsbs  21122  obslbs  21695  islbs4  21797  leordtvallem1  23153  trfbas2  23786  isclmp  25053  lssbn  25309  sineq0  26490  dchrelbas3  27206  elno3  27624  nb3grpr2  29367  uspgr2wlkeq  29631  2spthd  29928  clwwlknonwwlknonb  30092  frgr2wwlkeu  30313  elicoelioo  32760  cndprobprob  34475  bnj543  34929  cusgr3cyclex  35163  ellimits  35933  refsymrel2  38590  refsymrel3  38591  dfeqvrel2  38613  dfeqvrel3  38614  i0oii  48861