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

Theorem 3anan12 986
Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
3anan12

Proof of Theorem 3anan12
StepHypRef Expression
1 3ancoma 980 . 2
2 3anass 977 . 2
31, 2bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  /\w3a 973
This theorem is referenced by:  an33rean  1342  2reu5lem3  3307  fncnv  5657  dff1o2  5826  ixxun  11574  mreexexlem4d  15044  unocv  18711  iunocv  18712  mbfmax  22056  ulm2  22780  usgra2wlkspthlem2  24620  wwlknprop  24686  wwlknfi  24738  eclclwwlkn1  24832  numclwwlkovf2  25084  numclwlk1lem2f1  25094  pridlnr  30433  sineq0ALT  33737  bnj548  33955
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