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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1088 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1096 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 277 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1086
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 397  df-3an 1088
This theorem is referenced by:  3anrot  1099  an33reanOLD  1483  elioore  13109  leexp2  13889  swrdswrd  14418  pcgcd  16579  ablsubsub23  19426  xmetrtri  23508  phtpcer  24158  ishl2  24534  rusgrprc  27957  clwwlknon2num  28469  ablo32  28911  ablodivdiv  28915  ablodiv32  28917  bnj268  32688  bnj945  32753  bnj944  32918  bnj969  32926  loop1cycl  33099  btwncom  34316  btwnswapid2  34320  btwnouttr  34326  cgr3permute1  34350  colinearperm1  34364  endofsegid  34387  colinbtwnle  34420  broutsideof2  34424  outsideofcom  34430  neificl  35911  lhpexle2  38024  dfsucon  41130  uunTT1p1  42414  uun123  42428  smflimlem4  44309  ichexmpl1  44921  prproropf1o  44959  alsi-no-surprise  46500
  Copyright terms: Public domain W3C validator