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

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

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

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  1695  cbvexvw  1811  hbn1fw  1813  excom  1850  cbvex  2023  cbvex2  2029  nabbiOLD  2791  cbvrexf  3079  cbvrexcsf  3463  elsymdifxor  3731  symdifass  3734  dfss4  3739  indifdir  3761  difprsnss  4167  brdif  4506  otiunsndisj  4762  difopab  5144  rexiunxp  5153  rexxpf  5160  somin1  5410  cnvdif  5419  difxp  5438  imadif  5669  brprcneu  5865  dffv2  5946  ovima0  6453  porpss  6583  tfinds  6693  poxp  6911  tz7.48lem  7124  brsdom  7557  brsdom2  7660  fimax2g  7784  ordunifi  7788  dfsup2  7920  dfsup2OLD  7921  supgtoreq  7946  suc11reg  8053  rankxplim2  8315  rankxplim3  8316  alephval3  8508  kmlem4  8550  cflim2  8660  isfin4-2  8711  fin23lem25  8721  fin1a2lem5  8801  fin12  8810  axcclem  8854  zorng  8901  infinf  8958  alephadd  8969  fpwwe2  9038  axpre-lttri  9559  dfinfmr  10540  infmsup  10541  infmrgelb  10543  infmrlb  10544  arch  10813  rpneg  11274  xmulcom  11483  xmulneg1  11486  xmulf  11489  xrinfmss2  11527  difreicc  11677  fzp1nel  11788  ssnn0fi  12097  fsuppmapnn0fiubex  12101  hashfun  12499  swrdccatin2  12724  incexc2  13662  f1omvdco3  16601  psgnunilem4  16649  0ringnnzr  18044  gsumcom3  19028  mdetunilem7  19247  fctop  19632  cctop  19634  ntreq0  19705  ordtbas2  19819  cmpcld  20029  hausdiag  20272  fbun  20467  fbfinnfr  20468  opnfbas  20469  fbasrn  20511  filuni  20512  ufinffr  20556  alexsubALTlem2  20674  ellogdm  23146  usgraidx2v  24520  2spotiundisj  25189  avril1  25298  shne0i  26493  chnlei  26530  cvnbtwn2  27333  cvnbtwn3  27334  cvnbtwn4  27335  chrelat2i  27411  atabs2i  27448  dmdbr5ati  27468  nmo  27511  disjdifprg  27575  eliccelico  27748  elicoelioo  27749  xrdifh  27751  tosglblem  27817  xrnarchi  27888  hasheuni  28257  cntnevol  28372  omssubadd  28444  eulerpartlemgs2  28516  ballotlem2  28624  ballotlemodife  28633  plymulx0  28701  erdszelem9  28840  dftr6  29397  fundmpss  29414  dfon2lem5  29436  dfon2lem8  29439  dfon2lem9  29440  wzel  29597  nodenselem7  29664  nocvxminlem  29667  elfuns  29770  tfrqfree  29806  df3nandALT1  30067  andnand1  30069  imnand2  30070  gtinf  30342  fdc  30443  nninfnub  30449  tsbi4  30748  ts3an2  30763  ts3an3  30764  ts3or1  30765  n0el  30805  ctbnfien  30956  rencldnfilem  30958  numinfctb  31256  compab  31554  icccncfext  31893  itgioocnicc  31979  fourierdlem42  32134  fourierdlem62  32154  fourierdlem93  32185  fourierdlem101  32193  otiunsndisjX  32565  usgedgvadf1  32677  usgedgvadf1ALT  32680  zfregs2VD  33784  undif3VD  33825  onfrALTlem5VD  33828  sineq0ALT  33880  bnj1143  33992  bnj1304  34021  bnj1476  34048  bnj1533  34053  bnj1174  34202  bnj1204  34211  bnj1280  34219  bj-cbvexv  34440  bj-cbvex2v  34446  lcvnbtwn2  34895  lcvnbtwn3  34896  cvrnbtwn3  35144  dalem18  35548  lhpocnel2  35886  cdleme0nex  36158  cdlemk19w  36841  dihglblem6  37210  dvh2dim  37315  dvh3dim3N  37319  ifpnorcor  37877  ifpnancor  37883  ifpananb  37891  ifpxorxorb  37893  ifpdfnan  37894  ifpnannanb  37895  rp-fakenanass  37899  rp-isfinite6  37904  pwinfig  37906