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

Theorem 3ancomb 1040
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3ancomb ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))

Proof of Theorem 3ancomb
StepHypRef Expression
1 3ancoma 1038 . 2 ((𝜑𝜓𝜒) ↔ (𝜓𝜑𝜒))
2 3anrot 1036 . 2 ((𝜓𝜑𝜒) ↔ (𝜑𝜒𝜓))
31, 2bitri 263 1 ((𝜑𝜓𝜒) ↔ (𝜑𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  3simpb  1052  an33rean  1438  elioore  12076  leexp2  12777  swrdswrd  13312  pcgcd  15420  ablsubsub23  18053  xmetrtri  21970  phtpcer  22602  phtpcerOLD  22603  ishl2  22974  frgra3v  26529  numclwwlkovf2num  26612  ablo32  26787  ablodivdiv  26791  ablodiv32  26793  bnj268  30028  bnj945  30098  bnj944  30262  bnj969  30270  btwncom  31291  btwnswapid2  31295  btwnouttr  31301  cgr3permute1  31325  colinearperm1  31339  endofsegid  31362  colinbtwnle  31395  broutsideof2  31399  outsideofcom  31405  neificl  32719  lhpexle2  34314  uunTT1p1  38042  uun123  38056  smflimlem4  39660  rusgrprc  40790  av-numclwwlkovf2num  41516  alsi-no-surprise  42351
  Copyright terms: Public domain W3C validator