Theorem notbii 298

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	|- ( ph <-> ps )

Assertion

Ref	Expression
notbii	|- ( -. ph <-> -. ps )

Proof of Theorem notbii

Step	Hyp	Ref	Expression
1		notbii.1	. 2 |- ( ph <-> ps )
2		notbi 297	. 2 |- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
3	1, 2	mpbi 212	1 |- ( -. ph <-> -. ps )

Syntax hints:   -. wn 3   <-> wb 188

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 189

This theorem is referenced by:  sylnbi  308  xchnxbi  310  xchbinx  312  oplem1  973  nancomOLD  1384  xorcom  1404  xorassOLD  1406  xorneg2OLD  1415  xorbi12i  1417  trunanfalOLD  1484  falxortruOLD  1490  nic-axALT  1554  tbw-bijust  1578  rb-bijust  1629  19.43OLD  1739  cbvexvw  1861  hbn1fw  1863  excom  1900  excomOLD  1901  cbvex  2077  cbvex2  2083  nabbiOLD  2760  cbvrexf  3051  cbvrexcsf  3429  elsymdifxor  3700  symdifass  3703  dfss4  3708  indifdir  3730  difprsnss  4133  brdif  4472  otiunsndisj  4724  difopab  4983  rexiunxp  4992  rexxpf  4999  somin1  5250  cnvdif  5259  difxp  5278  imadif  5674  brprcneu  5872  dffv2  5952  ovima0  6460  porpss  6587  tfinds  6698  poxp  6917  tz7.48lem  7164  brsdom  7597  brsdom2  7700  fimax2g  7821  ordunifi  7825  dfsup2  7962  supgtoreq  7990  infcllem  8007  suc11reg  8128  rankxplim2  8354  rankxplim3  8355  alephval3  8543  kmlem4  8585  cflim2  8695  isfin4-2  8746  fin23lem25  8756  fin1a2lem5  8836  fin12  8845  axcclem  8889  zorng  8936  infinf  8993  alephadd  9004  fpwwe2  9070  axpre-lttri  9591  dfinfre  10590  dfinfmrOLD  10591  infrenegsup  10593  infmsupOLD  10594  infmrgelbOLD  10597  infmrlbOLD  10599  arch  10868  rpneg  11334  xmulcom  11554  xmulneg1  11557  xmulf  11560  xrinfmss2  11598  difreicc  11766  fzp1nel  11880  ssnn0fi  12198  fsuppmapnn0fiubex  12205  hashfun  12608  swrdccatin2  12839  incexc2  13889  lcmftp  14602  f1omvdco3  17083  psgnunilem4  17131  0ringnnzr  18486  gsumcom3  19416  mdetunilem7  19635  fctop  20011  cctop  20013  ntreq0  20085  ordtbas2  20199  cmpcld  20409  hausdiag  20652  fbun  20847  fbfinnfr  20848  opnfbas  20849  fbasrn  20891  filuni  20892  ufinffr  20936  alexsubALTlem2  21055  ellogdm  23576  usgraidx2v  25112  2spotiundisj  25782  avril1  25892  shne0i  27093  chnlei  27130  cvnbtwn2  27932  cvnbtwn3  27933  cvnbtwn4  27934  chrelat2i  28010  atabs2i  28047  dmdbr5ati  28067  nmo  28113  disjdifprg  28181  eliccelico  28359  elicoelioo  28360  xrdifh  28362  f1ocnt  28376  tosglblem  28431  xrnarchi  28502  hasheuni  28908  cntnevol  29052  omssubaddOLD  29134  sitgaddlemb  29183  eulerpartlemgs2  29215  ballotlem2  29323  ballotlemodife  29332  plymulx0  29438  bnj1143  29604  bnj1304  29633  bnj1476  29660  bnj1533  29665  bnj1174  29814  bnj1204  29823  bnj1280  29831  erdszelem9  29924  dftr6  30391  fundmpss  30408  dfon2lem5  30434  dfon2lem8  30437  dfon2lem9  30438  wzel  30508  nodenselem7  30575  nocvxminlem  30578  elfuns  30681  dfrecs2  30716  gtinf  30974  df3nandALT1  31056  andnand1  31058  imnand2  31059  bj-cbvexv  31291  bj-cbvex2v  31297  fdc  31994  nninfnub  32000  tsbi4  32298  ts3an2  32313  ts3an3  32314  ts3or1  32315  n0el  32355  lcvnbtwn2  32518  lcvnbtwn3  32519  cvrnbtwn3  32767  dalem18  33171  lhpocnel2  33509  cdleme0nex  33781  cdlemk19w  34464  dihglblem6  34833  dvh2dim  34938  dvh3dim3N  34942  ctbnfien  35586  rencldnfilem  35588  numinfctb  35888  ifpnorcor  36050  ifpnancor  36051  ifpdfnan  36056  ifpananb  36076  ifpnannanb  36077  ifpxorxorb  36081  rp-fakenanass  36085  rp-isfinite6  36089  pwinfig  36091  iunrelexp0  36160  frege131  36454  frege133  36456  compab  36658  zfregs2VD  37104  undif3VD  37146  onfrALTlem5VD  37149  sineq0ALT  37201  ndisj2  37257  disjrnmpt2  37319  icccncfext  37591  itgioocnicc  37680  fourierdlem42  37838  fourierdlem42OLD  37839  fourierdlem62  37858  fourierdlem93  37889  fourierdlem101  37897  nltle2tri  38434  evennodd  38491  otiunsndisjX  38714  usgridx2v  38928  usgedgvadf1  39031  usgedgvadf1ALT  39034