Theorem notbii 674

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 672	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  684  xchnxbi  686  xchbinx  688  nndc  858  xorcom  1432  xordidc  1443  dcfromnotnotr  1492  dcfromcon  1493  sbn  2005  neirr  2411  dfrex2dc  2523  ddifstab  3339  dfss4st  3440  ssddif  3441  difin  3444  difundi  3459  difindiss  3461  indifdir  3463  rabeq0  3524  abeq0  3525  snprc  3734  difprsnss  3811  uni0b  3918  disjnim  4078  brdif  4142  unidif0  4257  dtruex  4657  dcextest  4679  difopab  4863  cnvdif  5143  imadiflem  5409  imadif  5410  brprcneu  5632  poxp  6396  finexdc  7091  snexxph  7148  infmoti  7226  ismkvnex  7353  pw1nel3  7448  onntri35  7454  netap  7472  prltlu  7706  recexprlemdisj  7849  axpre-apti  8104  dfinfre  9135  fzdifsuc  10315  fzp1nel  10338  swrdccatin2  11309  ntreq0  14855  bj-nnor  16330  bj-nndcALT  16354  nnti  16591