Theorem 3anan32 1093

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 1085	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 644	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3ancomb  1095  anandi3r  1099  rabssrabd  4060  dff1o3  6623  bropfvvvvlem  7788  tz7.49c  8084  ispos2  17560  lbsacsbs  19930  obslbs  20876  islbs4  20978  leordtvallem1  21820  trfbas2  22453  isclmp  23703  lssbn  23957  sineq0  25111  dchrelbas3  25816  nb3grpr2  27167  uspgr2wlkeq  27429  2spthd  27722  clwwlknonwwlknonb  27887  frgr2wwlkeu  28108  elicoelioo  30503  cndprobprob  31698  bnj543  32167  cusgr3cyclex  32385  elno3  33164  ellimits  33373  refsymrel2  35805  refsymrel3  35806  dfeqvrel2  35827  dfeqvrel3  35828