Theorem 3ancoma 1098

Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)

Assertion

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

Proof of Theorem 3ancoma

Step	Hyp	Ref	Expression
1		3anan12 1096	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1095	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anrot  1100  3anrev  1101  cadcomb  1614  f13dfv  7225  suppssfifsupp  9329  elfzmlbp  13562  elfzo2  13585  pythagtriplem2  16700  pythagtrip  16717  xpsfrnel  17458  fucinv  17876  setcinv  17990  xrsdsreclb  20881  ordthaus  22772  regr1lem2  23128  xmetrtri2  23746  clmvscom  24490  hlcomb  27608  nb3grpr2  28394  nb3gr2nb  28395  rusgrnumwwlkslem  28977  ablomuldiv  29557  nvscom  29634  cnvadj  30897  iocinif  31752  fzto1st  32022  psgnfzto1st  32024  bnj312  33413  cgr3permute1  34709  lineext  34737  colinbtwnle  34779  outsideofcom  34789  linecom  34811  linerflx2  34812  cdlemg33d  39245  uunT12p3  43206  ichexmpl2  45782  rngcinv  46399  rngcinvALTV  46411  ringcinv  46450  ringcinvALTV  46474