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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1087 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1095 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 277 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  w3a 1085
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 206  df-an 395  df-3an 1087
This theorem is referenced by:  3anrot  1098  an33reanOLD  1482  elioore  13358  leexp2  14140  swrdswrd  14659  pcgcd  16815  ablsubadd23  19722  ablsubsub23  19733  xmetrtri  24081  phtpcer  24741  ishl2  25118  rusgrprc  29114  clwwlknon2num  29625  ablo32  30069  ablodivdiv  30073  ablodiv32  30075  bnj268  34018  bnj945  34082  bnj944  34247  bnj969  34255  loop1cycl  34426  btwncom  35290  btwnswapid2  35294  btwnouttr  35300  cgr3permute1  35324  colinearperm1  35338  endofsegid  35361  colinbtwnle  35394  broutsideof2  35398  outsideofcom  35404  neificl  36924  lhpexle2  39184  faosnf0.11b  42480  dfsucon  42576  uunTT1p1  43857  uun123  43871  smflimlem4  45788  ichexmpl1  46435  prproropf1o  46473  alsi-no-surprise  47930
  Copyright terms: Public domain W3C validator