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  4037  dff1o3  6788  bropfvvvvlem  8043  tz7.49c  8387  ispos2  18250  lbsacsbs  21123  obslbs  21697  islbs4  21799  leordtvallem1  23166  trfbas2  23799  isclmp  25065  lssbn  25320  sineq0  26501  dchrelbas3  27217  elno3  27635  nb3grpr2  29468  uspgr2wlkeq  29731  2spthd  30026  clwwlknonwwlknonb  30193  frgr2wwlkeu  30414  elicoelioo  32869  cndprobprob  34616  bnj543  35069  cusgr3cyclex  35352  ellimits  36124  eldmxrncnvepres  38685  eldmxrncnvepres2  38686  refsymrel2  38902  refsymrel3  38903  dfeqvrel2  38925  dfeqvrel3  38926  i0oii  49279