Theorem notbii 288

Description: Negate both sides of a logical equivalence. (Contributed by NM, 5-Aug-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 287	. 2 |- ( ( ph <-> ps ) <-> ( -. ph <-> -. ps ) )
3	1, 2	mpbi 200	1 |- ( -. ph <-> -. ps )

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

This theorem is referenced by:  sylnbi  298  xchnxbi  300  xchbinx  302  oplem1  931  nancom  1296  xorcom  1313  xorass  1314  xorneg2  1318  xorbi12i  1320  trunanfal  1361  falxortru  1366  hadnot  1399  cadnot  1400  nic-axALT  1445  tbw-bijust  1469  rb-bijust  1520  19.43OLD  1613  cbvexvw  1713  hbn1fw  1715  excom  1752  cbvex  2038  cbvrexf  2887  cbvrexcsf  3272  dfss4  3535  indifdir  3557  difprsnss  3894  brdif  4220  tfinds  4798  difopab  4965  rexiunxp  4974  rexxpf  4979  somin1  5229  cnvdif  5237  imadif  5487  brprcneu  5680  dffv2  5755  difxp  6339  poxp  6417  porpss  6485  tz7.48lem  6657  brsdom  7089  brsdom2  7190  fimax2g  7312  ordunifi  7316  dfsup2  7405  dfsup2OLD  7406  suc11reg  7530  rankxplim2  7760  rankxplim3  7761  alephval3  7947  kmlem4  7989  cflim2  8099  isfin4-2  8150  fin23lem25  8160  fin1a2lem5  8240  fin12  8249  axcclem  8293  zorng  8340  infinf  8397  alephadd  8408  fpwwe2  8474  axpre-lttri  8996  dfinfmr  9941  infmsup  9942  infmrgelb  9944  infmrlb  9945  arch  10174  rpneg  10597  xmulcom  10801  xmulneg1  10804  xmulf  10807  xrinfmss2  10845  difreicc  10984  hashfun  11655  incexc2  12573  fctop  17023  cctop  17025  ntreq0  17096  ordtbas2  17209  cmpcld  17419  hausdiag  17630  fbun  17825  fbfinnfr  17826  opnfbas  17827  fbasrn  17869  filuni  17870  ufinffr  17914  alexsubALTlem2  18032  ellogdm  20483  usgraidx2v  21365  avril1  21710  shne0i  22903  chnlei  22940  cvnbtwn2  23743  cvnbtwn3  23744  cvnbtwn4  23745  chrelat2i  23821  atabs2i  23858  dmdbr5ati  23878  nmo  23926  disjdifprg  23970  eliccelico  24093  elicoelioo  24094  xrdifh  24096  tosglb  24145  xrnarchi  24207  hasheuni  24428  cntnevol  24535  sibfof  24607  ballotlem2  24699  ballotlemodife  24708  erdszelem9  24838  fzp1nel  25163  dftr6  25321  fundmpss  25336  dfon2lem5  25357  dfon2lem8  25360  dfon2lem9  25361  nodenselem7  25555  nocvxminlem  25558  symdifass  25585  dffun10  25667  elfuns  25668  tfrqfree  25704  df3nandALT1  26050  andnand1  26052  imnand2  26053  gtinf  26212  fdc  26339  nninfnub  26345  n0el  26598  ctbnfien  26769  rencldnfilem  26771  numinfctb  27136  f1omvdco3  27260  psgnunilem4  27288  gsumcom3  27322  compab  27511  otiunsndisj  27954  otiunsndisjX  27955  2spotiundisj  28165  zfregs2VD  28662  undif3VD  28703  onfrALTlem5VD  28706  bnj1143  28867  bnj1304  28897  bnj1476  28924  bnj1533  28929  bnj1174  29078  bnj1204  29087  bnj1280  29095  cbvexwAUX7  29224  sb8ewAUX7  29295  cbvexOLD7  29410  sbcomOLD7  29439  sb8eOLD7  29441  lcvnbtwn2  29510  lcvnbtwn3  29511  cvrnbtwn3  29759  dalem18  30163  lhpocnel2  30501  cdleme0nex  30772  cdlemk19w  31454  dihglblem6  31823  dvh2dim  31928  dvh3dim3N  31932

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178