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 645	. 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  4106  dff1o3  6868  bropfvvvvlem  8132  tz7.49c  8502  ispos2  18385  lbsacsbs  21181  obslbs  21773  islbs4  21875  leordtvallem1  23239  trfbas2  23872  isclmp  25149  lssbn  25405  sineq0  26584  dchrelbas3  27300  elno3  27718  nb3grpr2  29418  uspgr2wlkeq  29682  2spthd  29974  clwwlknonwwlknonb  30138  frgr2wwlkeu  30359  elicoelioo  32783  cndprobprob  34403  bnj543  34869  cusgr3cyclex  35104  ellimits  35874  refsymrel2  38523  refsymrel3  38524  dfeqvrel2  38546  dfeqvrel3  38547  i0oii  48599