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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1074 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1083 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 267 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  w3a 1072
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 1074
This theorem is referenced by:  3anrot  1087  3simpbOLD  1145  an33rean  1587  elioore  12390  leexp2  13101  swrdswrd  13652  pcgcd  15776  ablsubsub23  18422  xmetrtri  22353  phtpcer  22987  ishl2  23358  rusgrprc  26688  clwwlknon2num  27245  ablo32  27704  ablodivdiv  27708  ablodiv32  27710  bnj268  31076  bnj945  31143  bnj944  31307  bnj969  31315  btwncom  32419  btwnswapid2  32423  btwnouttr  32429  cgr3permute1  32453  colinearperm1  32467  endofsegid  32490  colinbtwnle  32523  broutsideof2  32527  outsideofcom  32533  neificl  33854  lhpexle2  35791  uunTT1p1  39515  uun123  39529  smflimlem4  41480  alsi-no-surprise  43047
  Copyright terms: Public domain W3C validator