Theorem notbii 670

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 668	. 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  680  xchnxbi  682  xchbinx  684  nndc  853  xorcom  1408  xordidc  1419  dcfromnotnotr  1468  dcfromcon  1469  sbn  1981  neirr  2387  dfrex2dc  2499  ddifstab  3313  dfss4st  3414  ssddif  3415  difin  3418  difundi  3433  difindiss  3435  indifdir  3437  rabeq0  3498  abeq0  3499  snprc  3708  difprsnss  3782  uni0b  3889  disjnim  4049  brdif  4113  unidif0  4227  dtruex  4625  dcextest  4647  difopab  4829  cnvdif  5108  imadiflem  5372  imadif  5373  brprcneu  5592  poxp  6341  finexdc  7025  snexxph  7078  infmoti  7156  ismkvnex  7283  pw1nel3  7377  onntri35  7383  netap  7401  prltlu  7635  recexprlemdisj  7778  axpre-apti  8033  dfinfre  9064  fzdifsuc  10238  fzp1nel  10261  swrdccatin2  11220  ntreq0  14719  bj-nnor  15870  bj-nndcALT  15894  nnti  16129