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

Theorem an32 798
Description: A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
Assertion
Ref Expression
an32

Proof of Theorem an32
StepHypRef Expression
1 anass 649 . 2
2 an12 797 . 2
3 ancom 450 . 2
41, 2, 33bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  an32s  804  3anan32  985  indifdir  3753  inrab2  3770  reupick  3781  difxp  5436  resco  5516  imadif  5668  respreima  6016  dff1o6  6181  dfoprab2  6343  f11o  6762  mpt2curryd  7017  xpassen  7631  dfac5lem1  8525  kmlem3  8553  qbtwnre  11427  elioomnf  11648  modfsummod  13608  pcqcl  14380  tosso  15666  subgdmdprd  17081  opsrtoslem1  18148  pjfval2  18740  fvmptnn04if  19350  cmpcov2  19890  tx1cn  20110  tgphaus  20615  isms2  20953  elcncf1di  21399  elii1  21435  dvreslem  22313  dvdsflsumcom  23464  is2wlk  24567  cvnbtwn3  27207  ordtconlem1  27906  1stmbfm  28231  eulerpartlemn  28320  ballotlem2  28427  dfon3  29542  brsegle2  29759  bddiblnc  30085  ftc1anc  30098  prtlem17  30617  pm11.6  31298  stoweidlem17  31799  lcvnbtwn3  34753  cvrnbtwn3  35001  islpln5  35259  islvol5  35303  lhpexle3  35736  dibelval3  36874  dihglb2  37069
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
  Copyright terms: Public domain W3C validator