Theorem 3ancoma 1097

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 1095	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1094	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 278	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:  3anrot  1099  3anrev  1100  cadcomb  1614  f13dfv  7216  suppssfifsupp  9273  elfzmlbp  13543  elfzo2  13566  pythagtriplem2  16733  pythagtrip  16750  xpsfrnel  17470  fucinv  17887  setcinv  18001  rngcinv  20556  ringcinv  20590  xrsdsreclb  21354  ordthaus  23302  regr1lem2  23658  xmetrtri2  24274  clmvscom  25020  hlcomb  28584  nb3grpr2  29365  nb3gr2nb  29366  rusgrnumwwlkslem  29954  ablomuldiv  30536  nvscom  30613  cnvadj  31876  iocinif  32770  fzto1st  33081  psgnfzto1st  33083  bnj312  34747  cgr3permute1  36115  lineext  36143  colinbtwnle  36185  outsideofcom  36195  linecom  36217  linerflx2  36218  cdlemg33d  40831  uunT12p3  44921  ichexmpl2  47597  grtriproplem  48066  grtrif1o  48069  rngcinvALTV  48403  ringcinvALTV  48437