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

Assertion

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

Proof of Theorem notbii

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

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

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 187

This theorem is referenced by:  sylnbi  306  xchnxbi  308  xchbinx  310  oplem1  967  nancomOLD  1351  xorcom  1371  xorassOLD  1373  xorneg2OLD  1382  xorbi12i  1384  trunanfalOLD  1453  falxortruOLD  1459  hadnotOLD  1478  cadnotOLD  1480  nic-axALT  1529  tbw-bijust  1553  rb-bijust  1604  19.43OLD  1717  cbvexvw  1836  hbn1fw  1838  excom  1875  cbvex  2051  cbvex2  2057  nabbiOLD  2740  cbvrexf  3031  cbvrexcsf  3408  elsymdifxor  3678  symdifass  3681  dfss4  3686  indifdir  3708  difprsnss  4109  brdif  4447  otiunsndisj  4698  difopab  4957  rexiunxp  4966  rexxpf  4973  somin1  5223  cnvdif  5232  difxp  5251  imadif  5646  brprcneu  5844  dffv2  5924  ovima0  6437  porpss  6568  tfinds  6679  poxp  6898  tz7.48lem  7145  brsdom  7578  brsdom2  7681  fimax2g  7802  ordunifi  7806  dfsup2  7938  dfsup2OLD  7939  supgtoreq  7964  suc11reg  8071  rankxplim2  8332  rankxplim3  8333  alephval3  8525  kmlem4  8567  cflim2  8677  isfin4-2  8728  fin23lem25  8738  fin1a2lem5  8818  fin12  8827  axcclem  8871  zorng  8918  infinf  8975  alephadd  8986  fpwwe2  9053  axpre-lttri  9574  dfinfmr  10562  infmsup  10563  infmrgelb  10565  infmrlb  10566  arch  10835  rpneg  11297  xmulcom  11513  xmulneg1  11516  xmulf  11519  xrinfmss2  11557  difreicc  11708  fzp1nel  11819  ssnn0fi  12137  fsuppmapnn0fiubex  12144  hashfun  12546  swrdccatin2  12770  incexc2  13803  f1omvdco3  16800  psgnunilem4  16848  0ringnnzr  18239  gsumcom3  19195  mdetunilem7  19414  fctop  19799  cctop  19801  ntreq0  19873  ordtbas2  19987  cmpcld  20197  hausdiag  20440  fbun  20635  fbfinnfr  20636  opnfbas  20637  fbasrn  20679  filuni  20680  ufinffr  20724  alexsubALTlem2  20842  ellogdm  23316  usgraidx2v  24822  2spotiundisj  25491  avril1  25601  shne0i  26793  chnlei  26830  cvnbtwn2  27632  cvnbtwn3  27633  cvnbtwn4  27634  chrelat2i  27710  atabs2i  27747  dmdbr5ati  27767  nmo  27812  disjdifprg  27880  eliccelico  28049  elicoelioo  28050  xrdifh  28052  f1ocnt  28066  tosglblem  28122  xrnarchi  28193  hasheuni  28545  cntnevol  28689  omssubadd  28761  eulerpartlemgs2  28838  ballotlem2  28946  ballotlemodife  28955  plymulx0  29023  bnj1143  29189  bnj1304  29218  bnj1476  29245  bnj1533  29250  bnj1174  29399  bnj1204  29408  bnj1280  29416  erdszelem9  29509  dftr6  29976  fundmpss  29993  dfon2lem5  30019  dfon2lem8  30022  dfon2lem9  30023  wzel  30093  nodenselem7  30160  nocvxminlem  30163  elfuns  30266  dfrecs2  30301  gtinf  30560  df3nandALT1  30642  andnand1  30644  imnand2  30645  bj-cbvexv  30874  bj-cbvex2v  30880  fdc  31533  nninfnub  31539  tsbi4  31838  ts3an2  31853  ts3an3  31854  ts3or1  31855  n0el  31895  lcvnbtwn2  32058  lcvnbtwn3  32059  cvrnbtwn3  32307  dalem18  32711  lhpocnel2  33049  cdleme0nex  33321  cdlemk19w  34004  dihglblem6  34373  dvh2dim  34478  dvh3dim3N  34482  ctbnfien  35126  rencldnfilem  35128  numinfctb  35429  ifpnorcor  35584  ifpnancor  35585  ifpdfnan  35590  ifpananb  35610  ifpnannanb  35611  ifpxorxorb  35615  rp-fakenanass  35619  rp-isfinite6  35623  pwinfig  35625  iunrelexp0  35694  frege131  35988  frege133  35990  compab  36211  zfregs2VD  36684  undif3VD  36726  onfrALTlem5VD  36729  sineq0ALT  36781  icccncfext  37071  itgioocnicc  37157  fourierdlem42  37312  fourierdlem62  37332  fourierdlem93  37363  fourierdlem101  37371  nltle2tri  37680  evennodd  37739  otiunsndisjX  37947  usgedgvadf1  38057  usgedgvadf1ALT  38060