Theorem notbii 296

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 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  948  nancom  1329  xorcom  1346  xorass  1347  xorneg2  1354  xorbi12i  1356  trunanfal  1405  falxortru  1410  hadnot  1438  cadnot  1439  nic-axALT  1484  tbw-bijust  1508  rb-bijust  1559  19.43OLD  1660  cbvexvw  1747  hbn1fw  1749  excom  1786  cbvex  1969  cbvex2  1975  nabbi  2696  cbvrexf  2932  cbvrexcsf  3308  dfss4  3572  indifdir  3594  difprsnss  3997  brdif  4330  difopab  4958  rexiunxp  4967  rexxpf  4974  somin1  5222  cnvdif  5231  difxp  5250  imadif  5481  brprcneu  5672  dffv2  5752  ovima0  6231  porpss  6353  tfinds  6459  poxp  6673  tz7.48lem  6882  brsdom  7320  brsdom2  7423  fimax2g  7546  ordunifi  7550  dfsup2  7680  dfsup2OLD  7681  suc11reg  7813  rankxplim2  8075  rankxplim3  8076  alephval3  8268  kmlem4  8310  cflim2  8420  isfin4-2  8471  fin23lem25  8481  fin1a2lem5  8561  fin12  8570  axcclem  8614  zorng  8661  infinf  8718  alephadd  8729  fpwwe2  8797  axpre-lttri  9319  dfinfmr  10294  infmsup  10295  infmrgelb  10297  infmrlb  10298  arch  10563  rpneg  11007  xmulcom  11216  xmulneg1  11219  xmulf  11222  xrinfmss2  11260  difreicc  11403  hashfun  12182  swrdccatin2  12361  incexc2  13283  f1omvdco3  15934  psgnunilem4  15982  gsumcom3  18140  mdetunilem7  18265  fctop  18449  cctop  18451  ntreq0  18522  ordtbas2  18636  cmpcld  18846  hausdiag  19059  fbun  19254  fbfinnfr  19255  opnfbas  19256  fbasrn  19298  filuni  19299  ufinffr  19343  alexsubALTlem2  19461  ellogdm  21968  usgraidx2v  23133  avril1  23478  shne0i  24673  chnlei  24710  cvnbtwn2  25513  cvnbtwn3  25514  cvnbtwn4  25515  chrelat2i  25591  atabs2i  25628  dmdbr5ati  25648  nmo  25692  disjdifprg  25742  disjunsn  25759  eliccelico  25889  elicoelioo  25890  xrdifh  25892  nn0min  25912  tosglblem  25952  xrnarchi  26024  hasheuni  26387  cntnevol  26495  sibfof  26573  eulerpartlemgs2  26610  ballotlem2  26718  ballotlemodife  26727  plymulx0  26795  erdszelem9  26934  fzp1nel  27243  dftr6  27406  pocnv  27420  fundmpss  27423  dfon2lem5  27446  dfon2lem8  27449  dfon2lem9  27450  wzel  27607  nodenselem7  27674  nocvxminlem  27677  symdifass  27704  elfuns  27792  tfrqfree  27828  df3nandALT1  28089  andnand1  28091  imnand2  28092  gtinf  28355  fdc  28482  nninfnub  28488  notornotel2  28740  sbcni  28758  tsbi4  28788  ts3an2  28803  ts3an3  28804  ts3or1  28805  n0el  28846  ctbnfien  28999  rencldnfilem  29001  numinfctb  29301  compab  29539  otiunsndisj  29975  otiunsndisjX  29976  2spotiundisj  30498  0rngnnzr  30606  zfregs2VD  31276  undif3VD  31317  onfrALTlem5VD  31320  sineq0ALT  31372  bnj1143  31483  bnj1304  31512  bnj1476  31539  bnj1533  31544  bnj1174  31693  bnj1204  31702  bnj1280  31710  bj-cbvexv  31861  bj-cbvex2v  31867  lcvnbtwn2  32242  lcvnbtwn3  32243  cvrnbtwn3  32491  dalem18  32895  lhpocnel2  33233  cdleme0nex  33504  cdlemk19w  34186  dihglblem6  34555  dvh2dim  34660  dvh3dim3N  34664