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

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

Proof of Theorem 3ancomb
StepHypRef Expression
1 df-3an 1090 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3anan32 1098 . 2 ((𝜑𝜒𝜓) ↔ ((𝜑𝜓) ∧ 𝜒))
31, 2bitr4i 278 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3anrot  1101  an33reanOLD  1485  elioore  13350  leexp2  14132  swrdswrd  14651  pcgcd  16807  ablsubadd23  19673  ablsubsub23  19684  xmetrtri  23843  phtpcer  24493  ishl2  24869  rusgrprc  28827  clwwlknon2num  29338  ablo32  29780  ablodivdiv  29784  ablodiv32  29786  bnj268  33658  bnj945  33722  bnj944  33887  bnj969  33895  loop1cycl  34066  btwncom  34924  btwnswapid2  34928  btwnouttr  34934  cgr3permute1  34958  colinearperm1  34972  endofsegid  34995  colinbtwnle  35028  broutsideof2  35032  outsideofcom  35038  neificl  36559  lhpexle2  38819  faosnf0.11b  42111  dfsucon  42207  uunTT1p1  43488  uun123  43502  smflimlem4  45425  ichexmpl1  46072  prproropf1o  46110  alsi-no-surprise  47745
  Copyright terms: Public domain W3C validator