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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1086 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1094 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 277 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  3anrot  1097  elioore  13408  leexp2  14190  swrdswrd  14713  pcgcd  16880  ablsubadd23  19811  ablsubsub23  19822  xmetrtri  24352  phtpcer  25012  ishl2  25389  rusgrprc  29527  clwwlknon2num  30038  ablo32  30482  ablodivdiv  30486  ablodiv32  30488  bnj268  34554  bnj945  34618  bnj944  34783  bnj969  34791  loop1cycl  34965  btwncom  35838  btwnswapid2  35842  btwnouttr  35848  cgr3permute1  35872  colinearperm1  35886  endofsegid  35909  colinbtwnle  35942  broutsideof2  35946  outsideofcom  35952  neificl  37454  lhpexle2  39709  faosnf0.11b  43094  dfsucon  43190  uunTT1p1  44470  uun123  44484  smflimlem4  46395  ichexmpl1  47041  prproropf1o  47079  alsi-no-surprise  48544
  Copyright terms: Public domain W3C validator