Theorem notbii 287

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

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

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 177

This theorem is referenced by:  sylnbi  297  xchnxbi  299  xchbinx  301  oplem1  930  nancom  1290  xorcom  1307  xorass  1308  xorneg2  1312  xorbi12i  1314  trunanfal  1355  falxortru  1360  hadnot  1393  cadnot  1394  nic-axALT  1439  tbw-bijust  1463  rb-bijust  1514  19.43OLD  1606  cbvexvw  1703  excom  1741  cbvex  1985  sb8e  2093  cbvrexf  2831  cbvrexcsf  3200  dfss4  3490  indifdir  3512  complab  3525  difprsnss  3847  pw1disj  4168  dfimak2  4299  dfint3  4319  dfpw2  4328  dfiota4  4373  dfaddc2  4382  dfnnc2  4396  0nelsuc  4401  nnsucelrlem1  4425  nndisjeq  4430  preaddccan2lem1  4455  ltfinex  4465  eqpwrelk  4479  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  sfinltfin  4536  spfinex  4538  dfop2lem1  4574  brdif  4695  setconslem7  4738  dfswap2  4742  rexiunxp  4825  rexxpf  4829  dmeq0  4923  intirr  5030  cnvdif  5035  imadif  5172  ndmovcl  5615  epprc  5828  funsex  5829  transex  5911  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  qsexg  5983  el2c  6192  nmembers1lem3  6271  nchoicelem11  6300  nchoicelem16  6305  fnfreclem1  6318