Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ancoma Structured version   Visualization version   GIF version

Theorem 3ancoma 1095
 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
StepHypRef Expression
1 3anan12 1093 . 2 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
2 3anass 1092 . 2 ((𝜓𝜑𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitr4i 281 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084 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 400  df-3an 1086 This theorem is referenced by:  3anrot  1097  3anrev  1098  cadcomb  1615  f13dfv  7019  suppssfifsupp  8850  elfzmlbp  13033  elfzo2  13056  pythagtriplem2  16164  pythagtrip  16181  xpsfrnel  16847  fucinv  17255  setcinv  17362  xrsdsreclb  20159  ordthaus  22030  regr1lem2  22386  xmetrtri2  23004  clmvscom  23736  hlcomb  26441  nb3grpr2  27217  nb3gr2nb  27218  rusgrnumwwlkslem  27799  ablomuldiv  28379  nvscom  28456  cnvadj  29719  iocinif  30574  fzto1st  30844  psgnfzto1st  30846  bnj312  32158  cgr3permute1  33769  lineext  33797  colinbtwnle  33839  outsideofcom  33849  linecom  33871  linerflx2  33872  cdlemg33d  38156  uunT12p3  41679  ichexmpl2  44155  rngcinv  44773  rngcinvALTV  44785  ringcinv  44824  ringcinvALTV  44848
 Copyright terms: Public domain W3C validator