Theorem notbii 657

Description: Equivalence property for negation. Inference form. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
notbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
notbii	⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Proof of Theorem notbii

Step	Hyp	Ref	Expression
1		notbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		notbi 655	. 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnbi  667  xchnxbi  669  xchbinx  671  nndc  836  xorcom  1366  xordidc  1377  sbn  1925  neirr  2317  dfrex2dc  2428  ddifstab  3208  dfss4st  3309  ssddif  3310  difin  3313  difundi  3328  difindiss  3330  indifdir  3332  rabeq0  3392  abeq0  3393  snprc  3588  difprsnss  3658  uni0b  3761  disjnim  3920  brdif  3981  unidif0  4091  dtruex  4474  dcextest  4495  difopab  4672  cnvdif  4945  imadiflem  5202  imadif  5203  brprcneu  5414  poxp  6129  finexdc  6796  snexxph  6838  infmoti  6915  ismkvnex  7029  prltlu  7295  recexprlemdisj  7438  axpre-apti  7693  dfinfre  8714  fzdifsuc  9861  fzp1nel  9884  ntreq0  12301  bj-nnor  12946  bj-nndcALT  12963  nnti  13191