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  685  xchnxbi  687  xchbinx  689  nndc  859  xorcom  1433  xordidc  1444  dcfromnotnotr  1493  dcfromcon  1494  sbn  2006  neirr  2421  dfrex2dc  2533  ddifstab  3351  dfss4st  3454  ssddif  3455  difin  3458  difundi  3473  difindiss  3475  indifdir  3477  rabeq0  3538  abeq0  3539  snprc  3754  difprsnss  3832  uni0b  3939  disjnim  4099  brdif  4163  unidif0  4280  dtruex  4681  dcextest  4703  difopab  4888  cnvdif  5169  imadiflem  5435  imadif  5436  brprcneu  5663  poxp  6428  finexdc  7160  snexxph  7220  infmoti  7319  ismkvnex  7446  pw1nel3  7541  onntri35  7547  netap  7568  prltlu  7802  recexprlemdisj  7945  axpre-apti  8200  dfinfre  9230  fzdifsuc  10415  fzp1nel  10438  swrdccatin2  11421  ntreq0  14997  bj-nnor  16506  bj-nndcALT  16530  nnti  16766