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  955  nancom  1336  xorcom  1353  xorass  1354  xorneg2  1361  xorbi12i  1363  trunanfal  1412  falxortru  1417  hadnot  1435  cadnot  1436  nic-axALT  1481  tbw-bijust  1505  rb-bijust  1556  19.43OLD  1661  cbvexvw  1748  hbn1fw  1750  excom  1787  cbvex  1970  cbvex2  1976  nabbi  2727  cbvrexf  2963  cbvrexcsf  3341  dfss4  3605  indifdir  3627  difprsnss  4030  brdif  4363  difopab  4992  rexiunxp  5001  rexxpf  5008  somin1  5255  cnvdif  5264  difxp  5283  imadif  5514  brprcneu  5705  dffv2  5785  ovima0  6263  porpss  6385  tfinds  6491  poxp  6705  tz7.48lem  6917  brsdom  7353  brsdom2  7456  fimax2g  7579  ordunifi  7583  dfsup2  7713  dfsup2OLD  7714  suc11reg  7846  rankxplim2  8108  rankxplim3  8109  alephval3  8301  kmlem4  8343  cflim2  8453  isfin4-2  8504  fin23lem25  8514  fin1a2lem5  8594  fin12  8603  axcclem  8647  zorng  8694  infinf  8751  alephadd  8762  fpwwe2  8831  axpre-lttri  9353  dfinfmr  10328  infmsup  10329  infmrgelb  10331  infmrlb  10332  arch  10597  rpneg  11041  xmulcom  11250  xmulneg1  11253  xmulf  11256  xrinfmss2  11294  difreicc  11438  hashfun  12220  swrdccatin2  12399  incexc2  13322  f1omvdco3  15976  psgnunilem4  16024  gsumcom3  18321  mdetunilem7  18446  fctop  18630  cctop  18632  ntreq0  18703  ordtbas2  18817  cmpcld  19027  hausdiag  19240  fbun  19435  fbfinnfr  19436  opnfbas  19437  fbasrn  19479  filuni  19480  ufinffr  19524  alexsubALTlem2  19642  ellogdm  22106  usgraidx2v  23333  avril1  23678  shne0i  24873  chnlei  24910  cvnbtwn2  25713  cvnbtwn3  25714  cvnbtwn4  25715  chrelat2i  25791  atabs2i  25828  dmdbr5ati  25848  nmo  25891  disjdifprg  25941  disjunsn  25958  xrge0infss  26075  eliccelico  26089  elicoelioo  26090  xrdifh  26092  nn0min  26112  tosglblem  26152  xrnarchi  26223  hasheuni  26556  cntnevol  26664  sibfof  26748  eulerpartlemgs2  26785  ballotlem2  26893  ballotlemodife  26902  plymulx0  26970  erdszelem9  27109  fzp1nel  27419  dftr6  27582  pocnv  27596  fundmpss  27599  dfon2lem5  27622  dfon2lem8  27625  dfon2lem9  27626  wzel  27783  nodenselem7  27850  nocvxminlem  27853  symdifass  27880  elfuns  27968  tfrqfree  28004  df3nandALT1  28265  andnand1  28267  imnand2  28268  gtinf  28540  fdc  28667  nninfnub  28673  notornotel2  28925  sbcni  28943  tsbi4  28973  ts3an2  28988  ts3an3  28989  ts3or1  28990  n0el  29030  ctbnfien  29183  rencldnfilem  29185  numinfctb  29485  compab  29723  otiunsndisj  30158  otiunsndisjX  30159  2spotiundisj  30681  supgtoreq  30772  ssnn0fi  30775  0rngnnzr  30808  fsuppmapnn0fiubex  30830  zfregs2VD  31673  undif3VD  31714  onfrALTlem5VD  31717  sineq0ALT  31769  bnj1143  31880  bnj1304  31909  bnj1476  31936  bnj1533  31941  bnj1174  32090  bnj1204  32099  bnj1280  32107  bj-cbvexv  32329  bj-cbvex2v  32335  lcvnbtwn2  32768  lcvnbtwn3  32769  cvrnbtwn3  33017  dalem18  33421  lhpocnel2  33759  cdleme0nex  34030  cdlemk19w  34712  dihglblem6  35081  dvh2dim  35186  dvh3dim3N  35190