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  dcfromnotnotr  1458  dcfromcon  1459  sbn  1971  neirr  2376  dfrex2dc  2488  ddifstab  3296  dfss4st  3397  ssddif  3398  difin  3401  difundi  3416  difindiss  3418  indifdir  3420  rabeq0  3481  abeq0  3482  snprc  3688  difprsnss  3761  uni0b  3865  disjnim  4025  brdif  4087  unidif0  4201  dtruex  4596  dcextest  4618  difopab  4800  cnvdif  5077  imadiflem  5338  imadif  5339  brprcneu  5554  poxp  6299  finexdc  6972  snexxph  7025  infmoti  7103  ismkvnex  7230  pw1nel3  7316  onntri35  7322  netap  7339  prltlu  7573  recexprlemdisj  7716  axpre-apti  7971  dfinfre  9002  fzdifsuc  10175  fzp1nel  10198  ntreq0  14476  bj-nnor  15488  bj-nndcALT  15512  nnti  15747