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  2005  neirr  2412  dfrex2dc  2524  ddifstab  3341  dfss4st  3442  ssddif  3443  difin  3446  difundi  3461  difindiss  3463  indifdir  3465  rabeq0  3526  abeq0  3527  snprc  3738  difprsnss  3816  uni0b  3923  disjnim  4083  brdif  4147  unidif0  4263  dtruex  4663  dcextest  4685  difopab  4869  cnvdif  5150  imadiflem  5416  imadif  5417  brprcneu  5641  poxp  6406  finexdc  7135  snexxph  7192  infmoti  7270  ismkvnex  7397  pw1nel3  7492  onntri35  7498  netap  7516  prltlu  7750  recexprlemdisj  7893  axpre-apti  8148  dfinfre  9178  fzdifsuc  10361  fzp1nel  10384  swrdccatin2  11359  ntreq0  14926  bj-nnor  16435  bj-nndcALT  16459  nnti  16695