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

Theorem notbii 296
Description: Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
notbii.1
Assertion
Ref Expression
notbii

Proof of Theorem notbii
StepHypRef Expression
1 notbii.1 . 2
2 notbi 295 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
This theorem is referenced by:  sylnbi  306  xchnxbi  308  xchbinx  310  oplem1  964  nancomOLD  1347  xorcom  1366  xorass  1367  xorneg2  1374  xorbi12i  1376  trunanfal  1438  falxortru  1443  hadnot  1460  cadnot  1461  nic-axALT  1507  tbw-bijust  1531  rb-bijust  1582  19.43OLD  1694  cbvexvw  1810  hbn1fw  1812  excom  1849  cbvex  2022  cbvex2  2028  nabbiOLD  2791  cbvrexf  3079  cbvrexcsf  3467  dfss4  3731  indifdir  3753  difprsnss  4165  brdif  4502  otiunsndisj  4758  difopab  5139  rexiunxp  5148  rexxpf  5155  somin1  5408  cnvdif  5417  difxp  5436  imadif  5668  brprcneu  5864  dffv2  5946  ovima0  6454  porpss  6584  tfinds  6694  poxp  6912  tz7.48lem  7125  brsdom  7558  brsdom2  7661  fimax2g  7786  ordunifi  7790  dfsup2  7922  dfsup2OLD  7923  supgtoreq  7949  suc11reg  8057  rankxplim2  8319  rankxplim3  8320  alephval3  8512  kmlem4  8554  cflim2  8664  isfin4-2  8715  fin23lem25  8725  fin1a2lem5  8805  fin12  8814  axcclem  8858  zorng  8905  infinf  8962  alephadd  8973  fpwwe2  9042  axpre-lttri  9563  dfinfmr  10545  infmsup  10546  infmrgelb  10548  infmrlb  10549  arch  10817  rpneg  11278  xmulcom  11487  xmulneg1  11490  xmulf  11493  xrinfmss2  11531  difreicc  11681  fzp1nel  11791  ssnn0fi  12094  fsuppmapnn0fiubex  12098  hashfun  12495  swrdccatin2  12712  incexc2  13650  f1omvdco3  16474  psgnunilem4  16522  0ringnnzr  17917  gsumcom3  18901  mdetunilem7  19120  fctop  19505  cctop  19507  ntreq0  19578  ordtbas2  19692  cmpcld  19902  hausdiag  20146  fbun  20341  fbfinnfr  20342  opnfbas  20343  fbasrn  20385  filuni  20386  ufinffr  20430  alexsubALTlem2  20548  ellogdm  23020  usgraidx2v  24393  2spotiundisj  25062  avril1  25171  shne0i  26366  chnlei  26403  cvnbtwn2  27206  cvnbtwn3  27207  cvnbtwn4  27208  chrelat2i  27284  atabs2i  27321  dmdbr5ati  27341  nmo  27384  disjdifprg  27436  eliccelico  27588  elicoelioo  27589  xrdifh  27591  tosglblem  27657  xrnarchi  27728  hasheuni  28091  cntnevol  28199  eulerpartlemgs2  28319  ballotlem2  28427  ballotlemodife  28436  plymulx0  28504  erdszelem9  28643  dftr6  29179  fundmpss  29196  dfon2lem5  29219  dfon2lem8  29222  dfon2lem9  29223  wzel  29380  nodenselem7  29447  nocvxminlem  29450  symdifass  29477  elfuns  29565  tfrqfree  29601  df3nandALT1  29862  andnand1  29864  imnand2  29865  gtinf  30137  fdc  30238  nninfnub  30244  tsbi4  30543  ts3an2  30558  ts3an3  30559  ts3or1  30560  n0el  30600  ctbnfien  30752  rencldnfilem  30754  numinfctb  31052  compab  31350  icccncfext  31690  itgioocnicc  31776  fourierdlem42  31931  fourierdlem62  31951  fourierdlem93  31982  fourierdlem101  31990  otiunsndisjX  32301  usgedgvadf1  32415  usgedgvadf1ALT  32418  elsymdifxor  33217  zfregs2VD  33641  undif3VD  33682  onfrALTlem5VD  33685  sineq0ALT  33737  bnj1143  33849  bnj1304  33878  bnj1476  33905  bnj1533  33910  bnj1174  34059  bnj1204  34068  bnj1280  34076  bj-cbvexv  34297  bj-cbvex2v  34303  lcvnbtwn2  34752  lcvnbtwn3  34753  cvrnbtwn3  35001  dalem18  35405  lhpocnel2  35743  cdleme0nex  36015  cdlemk19w  36698  dihglblem6  37067  dvh2dim  37172  dvh3dim3N  37176  bj-ifananb  37731  bj-ifxorxorb  37733  bj-ifdfnan  37734  bj-ifnannanb  37735  rp-fakenanass  37739  rp-isfinite6  37744  pwinfig  37746
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
  Copyright terms: Public domain W3C validator