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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1083 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1091 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 279 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1081 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 208  df-an 397  df-3an 1083 This theorem is referenced by:  3anrot  1094  an33rean  1476  elioore  12763  leexp2  13530  swrdswrd  14062  pcgcd  16209  ablsubsub23  18881  xmetrtri  22899  phtpcer  23533  ishl2  23907  rusgrprc  27305  clwwlknon2num  27817  ablo32  28259  ablodivdiv  28263  ablodiv32  28265  bnj268  31884  bnj945  31950  bnj944  32115  bnj969  32123  loop1cycl  32287  btwncom  33378  btwnswapid2  33382  btwnouttr  33388  cgr3permute1  33412  colinearperm1  33426  endofsegid  33449  colinbtwnle  33482  broutsideof2  33486  outsideofcom  33492  neificl  34915  lhpexle2  37032  dfsucon  39773  uunTT1p1  41012  uun123  41026  smflimlem4  42935  ichexmpl1  43482  prproropf1o  43520  alsi-no-surprise  44799
 Copyright terms: Public domain W3C validator