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  962  nancom  1346  xorcom  1363  xorass  1364  xorneg2  1371  xorbi12i  1373  trunanfal  1422  falxortru  1427  hadnot  1445  cadnot  1446  nic-axALT  1491  tbw-bijust  1515  rb-bijust  1566  19.43OLD  1671  cbvexvw  1759  hbn1fw  1761  excom  1798  cbvex  1995  cbvex2  2001  nabbiOLD  2801  cbvrexf  3083  cbvrexcsf  3468  dfss4  3732  indifdir  3754  difprsnss  4162  brdif  4497  otiunsndisj  4753  difopab  5134  rexiunxp  5143  rexxpf  5150  somin1  5403  cnvdif  5412  difxp  5431  imadif  5663  brprcneu  5859  dffv2  5940  ovima0  6438  porpss  6568  tfinds  6678  poxp  6895  tz7.48lem  7106  brsdom  7538  brsdom2  7641  fimax2g  7766  ordunifi  7770  dfsup2  7902  dfsup2OLD  7903  supgtoreq  7928  suc11reg  8036  rankxplim2  8298  rankxplim3  8299  alephval3  8491  kmlem4  8533  cflim2  8643  isfin4-2  8694  fin23lem25  8704  fin1a2lem5  8784  fin12  8793  axcclem  8837  zorng  8884  infinf  8941  alephadd  8952  fpwwe2  9021  axpre-lttri  9542  dfinfmr  10520  infmsup  10521  infmrgelb  10523  infmrlb  10524  arch  10792  rpneg  11249  xmulcom  11458  xmulneg1  11461  xmulf  11464  xrinfmss2  11502  difreicc  11652  ssnn0fi  12062  fsuppmapnn0fiubex  12066  hashfun  12461  swrdccatin2  12675  incexc2  13613  f1omvdco3  16280  psgnunilem4  16328  0rngnnzr  17716  gsumcom3  18696  mdetunilem7  18915  fctop  19299  cctop  19301  ntreq0  19372  ordtbas2  19486  cmpcld  19696  hausdiag  19909  fbun  20104  fbfinnfr  20105  opnfbas  20106  fbasrn  20148  filuni  20149  ufinffr  20193  alexsubALTlem2  20311  ellogdm  22776  ltgov  23738  usgraidx2v  24097  2spotiundisj  24767  avril1  24875  shne0i  26070  chnlei  26107  cvnbtwn2  26910  cvnbtwn3  26911  cvnbtwn4  26912  chrelat2i  26988  atabs2i  27025  dmdbr5ati  27045  nmo  27088  disjdifprg  27137  disjunsn  27154  xrge0infss  27276  eliccelico  27284  elicoelioo  27285  xrdifh  27287  nn0min  27307  tosglblem  27347  xrnarchi  27418  hasheuni  27759  cntnevol  27867  sibfof  27950  eulerpartlemgs2  27987  ballotlem2  28095  ballotlemodife  28104  plymulx0  28172  erdszelem9  28311  fzp1nel  28621  dftr6  28784  pocnv  28798  fundmpss  28801  dfon2lem5  28824  dfon2lem8  28827  dfon2lem9  28828  wzel  28985  nodenselem7  29052  nocvxminlem  29055  symdifass  29082  elfuns  29170  tfrqfree  29206  df3nandALT1  29467  andnand1  29469  imnand2  29470  gtinf  29742  fdc  29869  nninfnub  29875  notornotel2  30127  sbcni  30145  tsbi4  30175  ts3an2  30190  ts3an3  30191  ts3or1  30192  n0el  30232  ctbnfien  30384  rencldnfilem  30386  numinfctb  30684  compab  30956  ralnex2  31045  icccncfext  31254  itgioocnicc  31323  fourierdlem42  31477  fourierdlem62  31497  fourierdlem93  31528  fourierdlem101  31536  otiunsndisjX  31796  usgedgvadf1  31910  usgedgvadf1ALT  31913  zfregs2VD  32739  undif3VD  32780  onfrALTlem5VD  32783  sineq0ALT  32835  bnj1143  32946  bnj1304  32975  bnj1476  33002  bnj1533  33007  bnj1174  33156  bnj1204  33165  bnj1280  33173  bj-cbvexv  33397  bj-cbvex2v  33403  lcvnbtwn2  33842  lcvnbtwn3  33843  cvrnbtwn3  34091  dalem18  34495  lhpocnel2  34833  cdleme0nex  35104  cdlemk19w  35786  dihglblem6  36155  dvh2dim  36260  dvh3dim3N  36264