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  4034  dff1o3  6770  bropfvvvvlem  8024  tz7.49c  8368  ispos2  18221  lbsacsbs  21063  obslbs  21637  islbs4  21739  leordtvallem1  23095  trfbas2  23728  isclmp  24995  lssbn  25250  sineq0  26431  dchrelbas3  27147  elno3  27565  nb3grpr2  29328  uspgr2wlkeq  29591  2spthd  29886  clwwlknonwwlknonb  30050  frgr2wwlkeu  30271  elicoelioo  32721  cndprobprob  34406  bnj543  34860  cusgr3cyclex  35113  ellimits  35888  eldmxrncnvepres  38386  eldmxrncnvepres2  38387  refsymrel2  38548  refsymrel3  38549  dfeqvrel2  38571  dfeqvrel3  38572  i0oii  48908