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	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
notbii	⊢ (¬ φ ↔ ¬ ψ)

Proof of Theorem notbii

Step	Hyp	Ref	Expression
1		notbii.1	. 2 ⊢ (φ ↔ ψ)
2		notbi 286	. 2 ⊢ ((φ ↔ ψ) ↔ (¬ φ ↔ ¬ ψ))
3	1, 2	mpbi 199	1 ⊢ (¬ φ ↔ ¬ ψ)

Syntax hints:  ¬ wn 3   ↔ wb 176

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 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  2830  cbvrexcsf  3199  dfss4  3489  indifdir  3511  complab  3524  difprsnss  3846  pw1disj  4167  dfimak2  4298  dfint3  4318  dfpw2  4327  dfiota4  4372  dfaddc2  4381  dfnnc2  4395  0nelsuc  4400  nnsucelrlem1  4424  nndisjeq  4429  preaddccan2lem1  4454  ltfinex  4464  eqpwrelk  4478  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  sfinltfin  4535  spfinex  4537  dfop2lem1  4573  brdif  4694  setconslem7  4737  dfswap2  4741  rexiunxp  4824  rexxpf  4828  dmeq0  4922  intirr  5029  cnvdif  5034  imadif  5171  ndmovcl  5614  epprc  5827  funsex  5828  transex  5910  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  qsexg  5982  el2c  6191  nmembers1lem3  6270  nchoicelem11  6299  nchoicelem16  6304  fnfreclem1  6317