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

Theorem 3ancoma 1038
 Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3ancoma ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))

Proof of Theorem 3ancoma
StepHypRef Expression
1 ancom 465 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 727 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 df-3an 1033 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
4 df-3an 1033 . 2 ((𝜓𝜑𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
52, 3, 43bitr4i 291 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  3ancomb  1040  3anrev  1042  3anan12  1044  3com12  1261  cadcomb  1543  f13dfv  6430  suppssfifsupp  8173  elfzmlbp  12319  elfzo2  12342  pythagtriplem2  15360  pythagtrip  15377  xpsfrnel  16046  fucinv  16456  setcinv  16563  xrsdsreclb  19612  ordthaus  20998  regr1lem2  21353  xmetrtri2  21971  clmvscom  22698  hlcomb  25298  nbgrasym  25968  nb3grapr2  25983  nb3gra2nb  25984  iswwlk  26211  rusgranumwlklem0  26475  frgra3v  26529  ablomuldiv  26790  nvscom  26868  cnvadj  28135  iocinif  28933  fzto1st  29184  psgnfzto1st  29186  bnj312  30031  cgr3permute1  31325  lineext  31353  colinbtwnle  31395  outsideofcom  31405  linecom  31427  linerflx2  31428  cdlemg33d  35015  uunT12p3  38050  nb3grpr2  40611  nb3gr2nb  40612  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848
 Copyright terms: Public domain W3C validator