Theorem 3anan32 1043

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 1033	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		an32 835	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
3	1, 2	bitri 263	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  anandi3r  1046  dff1o3  6056  bropfvvvvlem  7143  tz7.49c  7428  ispos2  16771  lbsacsbs  18977  obslbs  19893  islbs4  19990  leordtvallem1  20824  trfbas2  21457  isclmp  22705  lssbn  22956  sineq0  24077  dchrelbas3  24763  nb3grapr2  25983  usg2wlkeq  26236  elicoelioo  28930  cndprobprob  29827  bnj543  30217  elno3  31052  ellimits  31187  nb3grpr2  40611  uspgr2wlkeq  40854  2spthd  41148