Theorem notbii 669

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 667	. 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  679  xchnxbi  681  xchbinx  683  nndc  852  xorcom  1399  xordidc  1410  sbn  1968  neirr  2373  dfrex2dc  2485  ddifstab  3292  dfss4st  3393  ssddif  3394  difin  3397  difundi  3412  difindiss  3414  indifdir  3416  rabeq0  3477  abeq0  3478  snprc  3684  difprsnss  3757  uni0b  3861  disjnim  4021  brdif  4083  unidif0  4197  dtruex  4592  dcextest  4614  difopab  4796  cnvdif  5073  imadiflem  5334  imadif  5335  brprcneu  5548  poxp  6287  finexdc  6960  snexxph  7011  infmoti  7089  ismkvnex  7216  pw1nel3  7293  onntri35  7299  netap  7316  prltlu  7549  recexprlemdisj  7692  axpre-apti  7947  dfinfre  8977  fzdifsuc  10150  fzp1nel  10173  ntreq0  14311  bj-nnor  15296  bj-nndcALT  15320  nnti  15555