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

Theorem an32 775
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 632 . 2
2 an12 774 . 2
3 ancom 439 . 2
41, 2, 33bitri 264 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  /\wa 360
This theorem is referenced by:  an32s  781  3anan32  951  indifdir  3642  inrab2  3659  reupick  3670  difxp  5284  resco  5362  imadif  5511  respreima  5848  dff1o6  5994  dfoprab2  6145  f11o  6546  xpassen  7367  dfac5lem1  8175  kmlem3  8203  qbtwnre  11033  elioomnf  11247  pcqcl  13770  tosso  15047  subgdmdprd  16207  opsrtoslem1  17169  pjfval2  17561  cmpcov2  18467  tx1cn  18656  tgphaus  19161  isms2  19495  elcncf1di  19940  elii1  19975  dvreslem  20811  dvdsflsumcom  21994  is2wlk  22586  cvnbtwn3  24814  ordtconlem1  25533  1stmbfm  25855  eulerpartlemn  25938  ballotlem2  26021  dfon3  27076  brsegle2  27382  bddiblnc  27642  ftc1anc  27655  prtlem17  28165  pm11.6  28819  stoweidlem17  28991  modfsummod  29426  lcvnbtwn3  31376  cvrnbtwn3  31624  islpln5  31882  islvol5  31926  lhpexle3  32359  dibelval3  33495  dihglb2  33690
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 179  df-an 362
  Copyright terms: Public domain W3C validator