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

Theorem 3ancoma 1062
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 731 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
3 df-3an 1056 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
4 df-3an 1056 . 2 ((𝜓𝜑𝜒) ↔ ((𝜓𝜑) ∧ 𝜒))
52, 3, 43bitr4i 292 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  3ancomb  1064  3anrev  1067  3anan12  1069  3com12  1288  cadcomb  1592  f13dfv  6570  suppssfifsupp  8331  elfzmlbp  12489  elfzo2  12512  pythagtriplem2  15569  pythagtrip  15586  xpsfrnel  16270  fucinv  16680  setcinv  16787  xrsdsreclb  19841  ordthaus  21236  regr1lem2  21591  xmetrtri2  22208  clmvscom  22936  hlcomb  25543  nb3grpr2  26329  nb3gr2nb  26330  rusgrnumwwlkslem  26936  ablomuldiv  27534  nvscom  27612  cnvadj  28879  iocinif  29671  fzto1st  29981  psgnfzto1st  29983  bnj312  30906  cgr3permute1  32280  lineext  32308  colinbtwnle  32350  outsideofcom  32360  linecom  32382  linerflx2  32383  eldmqsres  34192  xrninxp2  34291  cdlemg33d  36314  uunT12p3  39346  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381
  Copyright terms: Public domain W3C validator