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

Theorem 3ancomb 1100
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1101 by Wolf Lammen, 9-Jun-2022.)
Assertion
Ref Expression
3ancomb ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1090 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1098 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 281 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1088
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 210  df-an 400  df-3an 1090
This theorem is referenced by:  3anrot  1101  an33reanOLD  1485  elioore  12844  leexp2  13620  swrdswrd  14149  pcgcd  16307  ablsubsub23  19057  xmetrtri  23101  phtpcer  23740  ishl2  24115  rusgrprc  27524  clwwlknon2num  28034  ablo32  28476  ablodivdiv  28480  ablodiv32  28482  bnj268  32250  bnj945  32316  bnj944  32481  bnj969  32489  loop1cycl  32662  btwncom  33946  btwnswapid2  33950  btwnouttr  33956  cgr3permute1  33980  colinearperm1  33994  endofsegid  34017  colinbtwnle  34050  broutsideof2  34054  outsideofcom  34060  neificl  35523  lhpexle2  37636  dfsucon  40668  uunTT1p1  41936  uun123  41950  smflimlem4  43832  ichexmpl1  44439  prproropf1o  44477  alsi-no-surprise  45937
  Copyright terms: Public domain W3C validator