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 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 105

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  3774  difprsnss  3853  uni0b  3960  disjnim  4120  brdif  4185  unidif0  4306  dtruex  4708  dcextest  4730  difopab  4915  cnvdif  5197  imadiflem  5463  imadif  5464  brprcneu  5691  poxp  6472  finexdc  7211  snexxph  7272  infmoti  7374  ismkvnex  7501  pw1nel3  7596  onntri35  7602  netap  7626  prltlu  7860  recexprlemdisj  8003  axpre-apti  8258  dfinfre  9294  fzdifsuc  10505  fzp1nel  10528  swrdccatin2  11523  ntreq0  15358  bj-nnor  16967  bj-nndcALT  16991  nnti  17227  wexmiddc  17247