Theorem notbii 678

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 676	. 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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  689  xchnxbi  691  xchbinx  693  nndc  863  xorcom  1437  xordidc  1448  dcfromnotnotr  1497  dcfromcon  1498  sbn  2012  neirr  2429  dfrex2dc  2541  ddifstab  3361  dfss4st  3464  ssddif  3465  difin  3468  difundi  3483  difindiss  3485  indifdir  3487  rabeq0  3552  abeq0  3553  snprc  3770  difprsnss  3848  uni0b  3955  disjnim  4115  brdif  4179  unidif0  4299  dtruex  4701  dcextest  4723  difopab  4908  cnvdif  5189  imadiflem  5455  imadif  5456  brprcneu  5683  poxp  6458  finexdc  7197  snexxph  7257  infmoti  7358  ismkvnex  7485  pw1nel3  7580  onntri35  7586  netap  7610  prltlu  7844  recexprlemdisj  7987  axpre-apti  8242  dfinfre  9276  fzdifsuc  10466  fzp1nel  10489  swrdccatin2  11479  ntreq0  15156  bj-nnor  16676  bj-nndcALT  16700  nnti  16936