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  4046  dff1o3  6806  bropfvvvvlem  8070  tz7.49c  8414  ispos2  18276  lbsacsbs  21066  obslbs  21639  islbs4  21741  leordtvallem1  23097  trfbas2  23730  isclmp  24997  lssbn  25252  sineq0  26433  dchrelbas3  27149  elno3  27567  nb3grpr2  29310  uspgr2wlkeq  29574  2spthd  29871  clwwlknonwwlknonb  30035  frgr2wwlkeu  30256  elicoelioo  32701  cndprobprob  34429  bnj543  34883  cusgr3cyclex  35123  ellimits  35898  eldmxrncnvepres  38396  eldmxrncnvepres2  38397  refsymrel2  38558  refsymrel3  38559  dfeqvrel2  38581  dfeqvrel3  38582  i0oii  48908