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

Theorem 3anan32 994
 Description: Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Assertion
Ref Expression
3anan32

Proof of Theorem 3anan32
StepHypRef Expression
1 df-3an 984 . 2
2 an32 805 . 2
31, 2bitri 252 1
 Colors of variables: wff setvar class Syntax hints:   wb 187   wa 370   w3a 982 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 188  df-an 372  df-3an 984 This theorem is referenced by:  anandi3r  997  dff1o3  5837  tz7.49c  7171  ispos2  16144  lbsacsbs  18314  obslbs  19224  islbs4  19321  leordtvallem1  20157  trfbas2  20789  lssbn  22212  sineq0  23341  dchrelbas3  24029  nb3grapr2  25027  usg2wlkeq  25281  elicoelioo  28196  cndprobprob  29097  bnj543  29492  elno3  30329  ellimits  30462
 Copyright terms: Public domain W3C validator