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

Theorem 3ancoma 1083
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 1081 . 2 ((𝜑𝜓𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
2 3anass 1080 . 2 ((𝜓𝜑𝜒) ↔ (𝜓 ∧ (𝜑𝜒)))
31, 2bitr4i 267 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  3anrot  1086  3anan12OLD  1087  3ancombOLD  1089  3anrev  1090  3com12OLD  1431  cadcomb  1700  f13dfv  6676  suppssfifsupp  8450  elfzmlbp  12658  elfzo2  12681  pythagtriplem2  15729  pythagtrip  15746  xpsfrnel  16431  fucinv  16840  setcinv  16947  xrsdsreclb  20008  ordthaus  21409  regr1lem2  21764  xmetrtri2  22381  clmvscom  23109  hlcomb  25719  nb3grpr2  26508  nb3gr2nb  26509  rusgrnumwwlkslem  27118  ablomuldiv  27746  nvscom  27824  cnvadj  29091  iocinif  29883  fzto1st  30193  psgnfzto1st  30195  bnj312  31118  cgr3permute1  32492  lineext  32520  colinbtwnle  32562  outsideofcom  32572  linecom  32594  linerflx2  32595  eldmqsres  34392  xrninxp2  34491  cdlemg33d  36517  uunT12p3  39552  rngcinv  42504  rngcinvALTV  42516  ringcinv  42555  ringcinvALTV  42579
  Copyright terms: Public domain W3C validator