Theorem 3ancoma 1038

Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3ancoma	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Proof of Theorem 3ancoma

Step	Hyp	Ref	Expression
1		ancom 465	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
2	1	anbi1i 727	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒))
3		df-3an 1033	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
4		df-3an 1033	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ ((𝜓 ∧ 𝜑) ∧ 𝜒))
5	2, 3, 4	3bitr4i 291	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:  3ancomb  1040  3anrev  1042  3anan12  1044  3com12  1261  cadcomb  1543  f13dfv  6430  suppssfifsupp  8173  elfzmlbp  12319  elfzo2  12342  pythagtriplem2  15360  pythagtrip  15377  xpsfrnel  16046  fucinv  16456  setcinv  16563  xrsdsreclb  19612  ordthaus  20998  regr1lem2  21353  xmetrtri2  21971  clmvscom  22698  hlcomb  25298  nbgrasym  25968  nb3grapr2  25983  nb3gra2nb  25984  iswwlk  26211  rusgranumwlklem0  26475  frgra3v  26529  ablomuldiv  26790  nvscom  26868  cnvadj  28135  iocinif  28933  fzto1st  29184  psgnfzto1st  29186  bnj312  30031  cgr3permute1  31325  lineext  31353  colinbtwnle  31395  outsideofcom  31405  linecom  31427  linerflx2  31428  cdlemg33d  35015  uunT12p3  38050  nb3grpr2  40611  nb3gr2nb  40612  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848