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  4033  dff1o3  6778  bropfvvvvlem  8031  tz7.49c  8375  ispos2  18236  lbsacsbs  21109  obslbs  21683  islbs4  21785  leordtvallem1  23152  trfbas2  23785  isclmp  25051  lssbn  25306  sineq0  26487  dchrelbas3  27203  elno3  27621  nb3grpr2  29405  uspgr2wlkeq  29668  2spthd  29963  clwwlknonwwlknonb  30130  frgr2wwlkeu  30351  elicoelioo  32807  cndprobprob  34544  bnj543  34998  cusgr3cyclex  35279  ellimits  36051  eldmxrncnvepres  38558  eldmxrncnvepres2  38559  refsymrel2  38763  refsymrel3  38764  dfeqvrel2  38786  dfeqvrel3  38787  i0oii  49107