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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1110 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1119 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 270 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  3anrot  1123  3simpbOLD  1182  an33rean  1608  elioore  12450  leexp2  13165  swrdswrd  13744  pcgcd  15911  ablsubsub23  18541  xmetrtri  22484  phtpcer  23118  ishl2  23492  rusgrprc  26831  clwwlknon2num  27435  ablo32  27920  ablodivdiv  27924  ablodiv32  27926  bnj268  31286  bnj945  31352  bnj944  31516  bnj969  31524  btwncom  32625  btwnswapid2  32629  btwnouttr  32635  cgr3permute1  32659  colinearperm1  32673  endofsegid  32696  colinbtwnle  32729  broutsideof2  32733  outsideofcom  32739  neificl  34027  lhpexle2  36022  uunTT1p1  39777  uun123  39791  smflimlem4  41715  alsi-no-surprise  43331
  Copyright terms: Public domain W3C validator