Theorem notbii 310

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 309	. 2 |- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
3	1, 2	mpbi 220	1 |- ( -. ph <-> -. ps )

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

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 197

This theorem is referenced by:  sylnbi  320  xchnxbi  322  xchbinx  324  oplem1  1007  xorcom  1467  xorbi12i  1477  nic-axALT  1599  tbw-bijust  1623  rb-bijust  1674  19.43OLD  1811  cbvexvw  1970  hbn1fw  1972  hba1w  1974  excom  2042  cbvexv1  2176  cbvex  2272  cbvexv  2275  cbvex2  2280  cbvrexf  3166  cbvrexcsf  3566  elsymdifxor  3850  symdifass  3853  dfss4  3858  indifdir  3883  neq0f  3926  n0el  3940  ab0  3951  pssdifcom2  4055  difprsnss  4329  brdif  4705  otiunsndisj  4980  difopab  5253  rexiunxp  5262  rexxpf  5269  somin1  5529  cnvdif  5539  difxp  5558  imadif  5973  brprcneu  6184  dffv2  6271  ovima0  6813  porpss  6941  tfinds  7059  poxp  7289  tz7.48lem  7536  brsdom  7978  brsdom2  8084  fimax2g  8206  ordunifi  8210  dfsup2  8350  supgtoreq  8376  infcllem  8393  suc11reg  8516  rankxplim2  8743  rankxplim3  8744  alephval3  8933  kmlem4  8975  cflim2  9085  isfin4-2  9136  fin23lem25  9146  fin1a2lem5  9226  fin12  9235  axcclem  9279  zorng  9326  infinf  9388  alephadd  9399  fpwwe2  9465  axpre-lttri  9986  dfinfre  11004  infrenegsup  11006  arch  11289  rpneg  11863  xmulcom  12096  xmulneg1  12099  xmulf  12102  xrinfmss2  12141  difreicc  12304  fzp1nel  12424  ssnn0fi  12784  fsuppmapnn0fiubex  12792  hashfun  13224  swrdccatin2  13487  s3iunsndisj  13707  incexc2  14570  lcmftp  15349  f1omvdco3  17869  psgnunilem4  17917  0ringnnzr  19269  gsumcom3  20205  mdetunilem7  20424  fctop  20808  cctop  20810  ntreq0  20881  ordtbas2  20995  cmpcld  21205  hausdiag  21448  fbun  21644  fbfinnfr  21645  opnfbas  21646  fbasrn  21688  filuni  21689  ufinffr  21733  alexsubALTlem2  21852  ellogdm  24385  numedglnl  26039  usgredg2v  26119  avril1  27319  shne0i  28307  chnlei  28344  cvnbtwn2  29146  cvnbtwn3  29147  cvnbtwn4  29148  chrelat2i  29224  atabs2i  29261  dmdbr5ati  29281  nmo  29325  difrab2  29339  disjdifprg  29388  eliccelico  29539  elicoelioo  29540  xrdifh  29542  f1ocnt  29559  tosglblem  29669  xrnarchi  29738  hasheuni  30147  cntnevol  30291  sitgaddlemb  30410  eulerpartlemgs2  30442  ballotlem2  30550  ballotlemodife  30559  plymulx0  30624  bnj1143  30861  bnj1304  30890  bnj1476  30917  bnj1533  30922  bnj1174  31071  bnj1204  31080  bnj1280  31088  erdszelem9  31181  dftr6  31640  fundmpss  31664  dfon2lem5  31692  dfon2lem8  31695  dfon2lem9  31696  wzel  31771  wzelOLD  31772  nosepon  31818  noextenddif  31821  nomaxmo  31847  nocvxminlem  31893  elfuns  32022  dfrecs2  32057  gtinfOLD  32314  df3nandALT1  32396  andnand1  32398  imnand2  32399  bj-notalbii  32598  bj-cbvex2v  32738  fdc  33541  nninfnub  33547  tsbi4  33943  ts3an2  33958  ts3an3  33959  ts3or1  33960  vvdifopab  34024  brvvdif  34027  n0elqs  34098  lcvnbtwn2  34314  lcvnbtwn3  34315  cvrnbtwn3  34563  dalem18  34967  lhpocnel2  35305  cdleme0nex  35577  cdlemk19w  36260  dihglblem6  36629  dvh2dim  36734  dvh3dim3N  36738  ctbnfien  37382  rencldnfilem  37384  numinfctb  37673  ifpnorcor  37825  ifpnancor  37826  ifpdfnan  37831  ifpananb  37851  ifpnannanb  37852  ifpxorxorb  37856  rp-fakenanass  37860  rp-isfinite6  37864  pwinfig  37866  elnonrel  37891  iunrelexp0  37994  frege131  38288  frege133  38290  compab  38645  zfregs2VD  39076  undif3VD  39118  onfrALTlem5VD  39121  sineq0ALT  39173  ndisj2  39218  disjrnmpt2  39375  uz0  39639  icccncfext  40100  itgioocnicc  40193  fourierdlem42  40366  fourierdlem62  40385  fourierdlem93  40416  fourierdlem101  40424  nsssmfmbf  40987  otiunsndisjX  41298  nltle2tri  41323  evennodd  41556  setrec2lem1  42440