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  3629  inrab2  3646  reupick  3657  difxp  5263  resco  5341  imadif  5490  respreima  5821  dff1o6  5958  dfoprab2  6109  f11o  6501  xpassen  7314  dfac5lem1  8118  kmlem3  8146  qbtwnre  10976  elioomnf  11190  pcqcl  13709  tosso  14984  subgdmdprd  16095  opsrtoslem1  17047  pjfval2  17439  cmpcov2  17956  tx1cn  18145  tgphaus  18650  isms2  18984  elcncf1di  19429  elii1  19464  dvreslem  20300  dvdsflsumcom  21482  is2wlk  22074  cvnbtwn3  24302  ordtconlem1  25024  1stmbfm  25346  eulerpartlemn  25429  ballotlem2  25512  dfon3  26567  brsegle2  26873  bddiblnc  27133  ftc1anc  27146  prtlem17  27656  pm11.6  28494  stoweidlem17  28666  modfsummod  29104  lcvnbtwn3  31099  cvrnbtwn3  31347  islpln5  31605  islvol5  31649  lhpexle3  32082  dibelval3  33218  dihglb2  33413
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