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  sbn  1964  neirr  2369  dfrex2dc  2481  ddifstab  3282  dfss4st  3383  ssddif  3384  difin  3387  difundi  3402  difindiss  3404  indifdir  3406  rabeq0  3467  abeq0  3468  snprc  3672  difprsnss  3745  uni0b  3849  disjnim  4009  brdif  4071  unidif0  4182  dtruex  4573  dcextest  4595  difopab  4775  cnvdif  5050  imadiflem  5310  imadif  5311  brprcneu  5523  poxp  6251  finexdc  6920  snexxph  6967  infmoti  7045  ismkvnex  7171  pw1nel3  7248  onntri35  7254  netap  7271  prltlu  7504  recexprlemdisj  7647  axpre-apti  7902  dfinfre  8931  fzdifsuc  10099  fzp1nel  10122  ntreq0  14029  bj-nnor  14883  bj-nndcALT  14907  nnti  15142