MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anrev Unicode version

Theorem 3anrev 984
Description: Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3anrev

Proof of Theorem 3anrev
StepHypRef Expression
1 3ancoma 980 . 2
2 3anrot 978 . 2
31, 2bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\w3a 973
This theorem is referenced by:  3com13  1201  an33rean  1342  nnmcan  7302  odupos  15765  frgra3v  25002  pocnv  29193  btwnswapid2  29668  colinbtwnle  29768  uunT11p2  33595  uunT12p5  33601  uun2221p2  33612  bnj345  33766  bnj1098  33842
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator