Theorem notbii 303

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

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

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 190

This theorem is referenced by:  sylnbi  313  xchnxbi  315  xchbinx  317  oplem1  976  xorcom  1433  xorassOLD  1435  xorneg2OLD  1444  xorbi12i  1446  trunanfalOLD  1496  falxortruOLD  1502  nic-axALT  1565  tbw-bijust  1589  rb-bijust  1640  19.43OLD  1754  cbvexvw  1887  hbn1fw  1889  excom  1944  excomOLD  1945  cbvexv1  2084  cbvex  2128  cbvex2  2134  cbvrexf  3000  cbvrexcsf  3382  elsymdifxor  3660  symdifass  3663  dfss4  3668  indifdir  3690  difprsnss  4098  brdif  4446  otiunsndisj  4707  difopab  4971  rexiunxp  4980  rexxpf  4987  somin1  5239  cnvdif  5248  difxp  5267  imadif  5668  brprcneu  5872  dffv2  5953  ovima0  6467  porpss  6594  tfinds  6705  poxp  6927  tz7.48lem  7176  brsdom  7610  brsdom2  7714  fimax2g  7835  ordunifi  7839  dfsup2  7976  supgtoreq  8004  infcllem  8021  suc11reg  8142  rankxplim2  8369  rankxplim3  8370  alephval3  8559  kmlem4  8601  cflim2  8711  isfin4-2  8762  fin23lem25  8772  fin1a2lem5  8852  fin12  8861  axcclem  8905  zorng  8952  infinf  9009  alephadd  9020  fpwwe2  9086  axpre-lttri  9607  dfinfre  10610  dfinfmrOLD  10611  infrenegsup  10613  infmsupOLD  10614  infmrgelbOLD  10617  infmrlbOLD  10619  arch  10890  rpneg  11355  xmulcom  11577  xmulneg1  11580  xmulf  11583  xrinfmss2  11621  difreicc  11790  fzp1nel  11904  ssnn0fi  12235  fsuppmapnn0fiubex  12242  hashfun  12650  swrdccatin2  12897  incexc2  13973  lcmftp  14688  f1omvdco3  17168  psgnunilem4  17216  0ringnnzr  18570  gsumcom3  19501  mdetunilem7  19720  fctop  20096  cctop  20098  ntreq0  20170  ordtbas2  20284  cmpcld  20494  hausdiag  20737  fbun  20933  fbfinnfr  20934  opnfbas  20935  fbasrn  20977  filuni  20978  ufinffr  21022  alexsubALTlem2  21141  ellogdm  23663  usgraidx2v  25199  2spotiundisj  25869  avril1  25979  shne0i  27182  chnlei  27219  cvnbtwn2  28021  cvnbtwn3  28022  cvnbtwn4  28023  chrelat2i  28099  atabs2i  28136  dmdbr5ati  28156  nmo  28200  disjdifprg  28262  eliccelico  28434  elicoelioo  28435  xrdifh  28437  f1ocnt  28451  tosglblem  28505  xrnarchi  28575  hasheuni  28980  cntnevol  29124  omssubaddOLD  29205  sitgaddlemb  29254  eulerpartlemgs2  29286  ballotlem2  29394  ballotlemodife  29403  plymulx0  29508  bnj1143  29674  bnj1304  29703  bnj1476  29730  bnj1533  29735  bnj1174  29884  bnj1204  29893  bnj1280  29901  erdszelem9  29994  dftr6  30461  fundmpss  30478  dfon2lem5  30504  dfon2lem8  30507  dfon2lem9  30508  wzel  30578  nosepon  30627  nodenselem7  30647  nocvxminlem  30650  elfuns  30753  dfrecs2  30788  gtinf  31046  df3nandALT1  31128  andnand1  31130  imnand2  31131  bj-cbvex2v  31405  fdc  32138  nninfnub  32144  tsbi4  32442  ts3an2  32457  ts3an3  32458  ts3or1  32459  n0el  32497  lcvnbtwn2  32664  lcvnbtwn3  32665  cvrnbtwn3  32913  dalem18  33317  lhpocnel2  33655  cdleme0nex  33927  cdlemk19w  34610  dihglblem6  34979  dvh2dim  35084  dvh3dim3N  35088  ctbnfien  35732  rencldnfilem  35734  numinfctb  36033  ifpnorcor  36195  ifpnancor  36196  ifpdfnan  36201  ifpananb  36221  ifpnannanb  36222  ifpxorxorb  36226  rp-fakenanass  36230  rp-isfinite6  36234  pwinfig  36236  elnonrel  36262  iunrelexp0  36365  frege131  36661  frege133  36663  compab  36864  zfregs2VD  37300  undif3VD  37342  onfrALTlem5VD  37345  sineq0ALT  37397  ndisj2  37448  disjrnmpt2  37534  icccncfext  37862  itgioocnicc  37951  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem62  38144  fourierdlem93  38175  fourierdlem101  38183  nltle2tri  38861  evennodd  38918  otiunsndisjX  39152  usgredg2v  39468  usgedgvadf1  40235  usgedgvadf1ALT  40238