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

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

Proof of Theorem 3ancoma
StepHypRef Expression
1 ancom 466 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
21anbi1i 730 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 df-3an 1038 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
4 df-3an 1038 . 2 ((𝜓𝜑𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
52, 3, 43bitr4i 292 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  3ancomb  1045  3anrev  1047  3anan12  1049  3com12  1266  cadcomb  1549  f13dfv  6484  suppssfifsupp  8234  elfzmlbp  12391  elfzo2  12414  pythagtriplem2  15446  pythagtrip  15463  xpsfrnel  16144  fucinv  16554  setcinv  16661  xrsdsreclb  19712  ordthaus  21098  regr1lem2  21453  xmetrtri2  22071  clmvscom  22798  hlcomb  25398  nb3grpr2  26172  nb3gr2nb  26173  rusgrnumwwlkslem  26731  ablomuldiv  27252  nvscom  27330  cnvadj  28597  iocinif  29384  fzto1st  29635  psgnfzto1st  29637  bnj312  30482  cgr3permute1  31794  lineext  31822  colinbtwnle  31864  outsideofcom  31874  linecom  31896  linerflx2  31897  cdlemg33d  35474  uunT12p3  38508  rngcinv  41266  rngcinvALTV  41278  ringcinv  41317  ringcinvALTV  41341
  Copyright terms: Public domain W3C validator