Theorem 3anan32 1095

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 1087	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 642	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3ancomb  1097  anandi3r  1101  rabssrabd  4012  dff1o3  6706  bropfvvvvlem  7902  tz7.49c  8247  ispos2  17948  lbsacsbs  20333  obslbs  20847  islbs4  20949  leordtvallem1  22269  trfbas2  22902  isclmp  24166  lssbn  24421  sineq0  25585  dchrelbas3  26291  nb3grpr2  27653  uspgr2wlkeq  27915  2spthd  28207  clwwlknonwwlknonb  28371  frgr2wwlkeu  28592  elicoelioo  31001  cndprobprob  32305  bnj543  32773  cusgr3cyclex  32998  elno3  33785  ellimits  34139  refsymrel2  36608  refsymrel3  36609  dfeqvrel2  36630  dfeqvrel3  36631  i0oii  46101