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 278 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  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 207  df-an 396  df-3an 1088
This theorem is referenced by:  3anrot  1099  elioore  13418  leexp2  14212  swrdswrd  14744  pcgcd  16917  ablsubadd23  19832  ablsubsub23  19843  xmetrtri  24366  phtpcer  25028  ishl2  25405  rusgrprc  29609  clwwlknon2num  30125  ablo32  30569  ablodivdiv  30573  ablodiv32  30575  bnj268  34724  bnj945  34788  bnj944  34953  bnj969  34961  loop1cycl  35143  btwncom  36016  btwnswapid2  36020  btwnouttr  36026  cgr3permute1  36050  colinearperm1  36064  endofsegid  36087  colinbtwnle  36120  broutsideof2  36124  outsideofcom  36130  neificl  37761  lhpexle2  40013  faosnf0.11b  43445  dfsucon  43541  uunTT1p1  44819  uun123  44833  smflimlem4  46794  ichexmpl1  47461  prproropf1o  47499  grtriproplem  47911  grtrif1o  47914  alsi-no-surprise  49370
  Copyright terms: Public domain W3C validator