Theorem 3ancoma 1113

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 1110	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
2		3anass 1109	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
3	1, 2	bitr4i 281	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anrot  1115  3anrev  1116  cadcomb  1636  f13dfv  7262  suppssfifsupp  9328  elfzmlbp  13655  elfzo2  13678  pythagtriplem2  16865  pythagtrip  16882  xpsfrnel  17604  fucinv  18021  setcinv  18135  rngcinv  20710  ringcinv  20744  xrsdsreclb  21521  ordthaus  23498  regr1lem2  23854  xmetrtri2  24470  clmvscom  25206  hlcomb  28826  nb3grpr2  29638  nb3gr2nb  29639  rusgrnumwwlkslem  30226  ablomuldiv  30809  nvscom  30886  cnvadj  32149  iocinif  33034  fzto1st  33331  psgnfzto1st  33333  bnj312  35013  cgr3permute1  36406  lineext  36434  colinbtwnle  36476  outsideofcom  36486  linecom  36508  linerflx2  36509  cdlemg33d  41340  uunT12p3  45369  ichexmpl2  48075  grtriproplem  48560  grtrif1o  48563  rngcinvALTV  48897  ringcinvALTV  48931