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  4093  dff1o3  6855  bropfvvvvlem  8115  tz7.49c  8485  ispos2  18373  lbsacsbs  21176  obslbs  21768  islbs4  21870  leordtvallem1  23234  trfbas2  23867  isclmp  25144  lssbn  25400  sineq0  26581  dchrelbas3  27297  elno3  27715  nb3grpr2  29415  uspgr2wlkeq  29679  2spthd  29971  clwwlknonwwlknonb  30135  frgr2wwlkeu  30356  elicoelioo  32787  cndprobprob  34420  bnj543  34886  cusgr3cyclex  35121  ellimits  35892  refsymrel2  38549  refsymrel3  38550  dfeqvrel2  38572  dfeqvrel3  38573  i0oii  48716