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  949  indifdir  3589  inrab2  3606  reupick  3617  resco  5424  imadif  5579  f11o  5759  respreima  5911  dff1o6  6065  dfoprab2  6175  difxp  6434  xpassen  7255  dfac5lem1  8059  kmlem3  8087  qbtwnre  10840  elioomnf  11054  pcqcl  13285  tosso  14520  subgdmdprd  15628  opsrtoslem1  16580  pjfval2  16972  cmpcov2  17489  tx1cn  17677  tgphaus  18182  isms2  18516  elcncf1di  18961  elii1  18996  dvreslem  19832  dvdsflsumcom  21009  is2wlk  21601  cvnbtwn3  23827  1stmbfm  24840  eulerpartlemn  24923  ballotlem2  25006  dfon3  25997  brsegle2  26303  bddiblnc  26542  ftc1anc  26555  prtlem17  27062  pm11.6  27903  stoweidlem17  28076  lcvnbtwn3  30222  cvrnbtwn3  30470  islpln5  30728  islvol5  30772  lhpexle3  31205  dibelval3  32341  dihglb2  32536
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