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  975  nancomOLD  1388  xorcom  1408  xorassOLD  1410  xorneg2OLD  1419  xorbi12i  1421  trunanfalOLD  1488  falxortruOLD  1494  nic-axALT  1557  tbw-bijust  1581  rb-bijust  1632  19.43OLD  1746  cbvexvw  1879  hbn1fw  1881  excom  1927  excomOLD  1928  cbvexv1  2065  cbvex  2115  cbvex2  2121  cbvrexf  3014  cbvrexcsf  3396  elsymdifxor  3669  symdifass  3672  dfss4  3677  indifdir  3699  difprsnss  4107  brdif  4453  otiunsndisj  4707  difopab  4966  rexiunxp  4975  rexxpf  4982  somin1  5233  cnvdif  5242  difxp  5261  imadif  5658  brprcneu  5858  dffv2  5938  ovima0  6448  porpss  6575  tfinds  6686  poxp  6908  tz7.48lem  7158  brsdom  7592  brsdom2  7696  fimax2g  7817  ordunifi  7821  dfsup2  7958  supgtoreq  7986  infcllem  8003  suc11reg  8124  rankxplim2  8351  rankxplim3  8352  alephval3  8541  kmlem4  8583  cflim2  8693  isfin4-2  8744  fin23lem25  8754  fin1a2lem5  8834  fin12  8843  axcclem  8887  zorng  8934  infinf  8991  alephadd  9002  fpwwe2  9068  axpre-lttri  9589  dfinfre  10588  dfinfmrOLD  10589  infrenegsup  10591  infmsupOLD  10592  infmrgelbOLD  10595  infmrlbOLD  10597  arch  10866  rpneg  11332  xmulcom  11552  xmulneg1  11555  xmulf  11558  xrinfmss2  11596  difreicc  11764  fzp1nel  11878  ssnn0fi  12197  fsuppmapnn0fiubex  12204  hashfun  12609  swrdccatin2  12843  incexc2  13896  lcmftp  14609  f1omvdco3  17090  psgnunilem4  17138  0ringnnzr  18493  gsumcom3  19424  mdetunilem7  19643  fctop  20019  cctop  20021  ntreq0  20093  ordtbas2  20207  cmpcld  20417  hausdiag  20660  fbun  20855  fbfinnfr  20856  opnfbas  20857  fbasrn  20899  filuni  20900  ufinffr  20944  alexsubALTlem2  21063  ellogdm  23584  usgraidx2v  25120  2spotiundisj  25790  avril1  25900  shne0i  27101  chnlei  27138  cvnbtwn2  27940  cvnbtwn3  27941  cvnbtwn4  27942  chrelat2i  28018  atabs2i  28055  dmdbr5ati  28075  nmo  28121  disjdifprg  28185  eliccelico  28359  elicoelioo  28360  xrdifh  28362  f1ocnt  28376  tosglblem  28430  xrnarchi  28501  hasheuni  28906  cntnevol  29050  omssubaddOLD  29132  sitgaddlemb  29181  eulerpartlemgs2  29213  ballotlem2  29321  ballotlemodife  29330  plymulx0  29436  bnj1143  29602  bnj1304  29631  bnj1476  29658  bnj1533  29663  bnj1174  29812  bnj1204  29821  bnj1280  29829  erdszelem9  29922  dftr6  30390  fundmpss  30407  dfon2lem5  30433  dfon2lem8  30436  dfon2lem9  30437  wzel  30507  nosepon  30556  nodenselem7  30576  nocvxminlem  30579  elfuns  30682  dfrecs2  30717  gtinf  30975  df3nandALT1  31057  andnand1  31059  imnand2  31060  bj-cbvex2v  31339  fdc  32074  nninfnub  32080  tsbi4  32378  ts3an2  32393  ts3an3  32394  ts3or1  32395  n0el  32433  lcvnbtwn2  32593  lcvnbtwn3  32594  cvrnbtwn3  32842  dalem18  33246  lhpocnel2  33584  cdleme0nex  33856  cdlemk19w  34539  dihglblem6  34908  dvh2dim  35013  dvh3dim3N  35017  ctbnfien  35661  rencldnfilem  35663  numinfctb  35962  ifpnorcor  36124  ifpnancor  36125  ifpdfnan  36130  ifpananb  36150  ifpnannanb  36151  ifpxorxorb  36155  rp-fakenanass  36159  rp-isfinite6  36163  pwinfig  36165  elnonrel  36191  iunrelexp0  36294  frege131  36590  frege133  36592  compab  36794  zfregs2VD  37237  undif3VD  37279  onfrALTlem5VD  37282  sineq0ALT  37334  ndisj2  37389  disjrnmpt2  37463  icccncfext  37765  itgioocnicc  37854  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem62  38032  fourierdlem93  38063  fourierdlem101  38071  nltle2tri  38716  evennodd  38773  otiunsndisjX  39006  usgredg2v  39304  usgedgvadf1  39780  usgedgvadf1ALT  39783