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  4035  dff1o3  6780  bropfvvvvlem  8033  tz7.49c  8377  ispos2  18238  lbsacsbs  21111  obslbs  21685  islbs4  21787  leordtvallem1  23154  trfbas2  23787  isclmp  25053  lssbn  25308  sineq0  26489  dchrelbas3  27205  elno3  27623  nb3grpr2  29456  uspgr2wlkeq  29719  2spthd  30014  clwwlknonwwlknonb  30181  frgr2wwlkeu  30402  elicoelioo  32858  cndprobprob  34595  bnj543  35049  cusgr3cyclex  35330  ellimits  36102  eldmxrncnvepres  38629  eldmxrncnvepres2  38630  refsymrel2  38834  refsymrel3  38835  dfeqvrel2  38857  dfeqvrel3  38858  i0oii  49175