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

Theorem 3ancoma 1092
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 1090 . 2 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
2 3anass 1089 . 2 ((𝜓𝜑𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitr4i 279 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  3anrot  1094  3anrev  1095  cadcomb  1607  f13dfv  7027  suppssfifsupp  8842  elfzmlbp  13013  elfzo2  13036  pythagtriplem2  16149  pythagtrip  16166  xpsfrnel  16830  fucinv  17238  setcinv  17345  xrsdsreclb  20527  ordthaus  21927  regr1lem2  22283  xmetrtri2  22900  clmvscom  23628  hlcomb  26322  nb3grpr2  27098  nb3gr2nb  27099  rusgrnumwwlkslem  27681  ablomuldiv  28262  nvscom  28339  cnvadj  29602  iocinif  30436  fzto1st  30678  psgnfzto1st  30680  bnj312  31887  cgr3permute1  33412  lineext  33440  colinbtwnle  33482  outsideofcom  33492  linecom  33514  linerflx2  33515  cdlemg33d  37731  uunT12p3  41020  ichexmpl2  43483  rngcinv  44154  rngcinvALTV  44166  ringcinv  44205  ringcinvALTV  44229
  Copyright terms: Public domain W3C validator