Theorem notbii 658

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 656	. 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3	1, 2	ax-mp 5	1 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnbi  668  xchnxbi  670  xchbinx  672  nndc  837  xorcom  1367  xordidc  1378  sbn  1926  neirr  2318  dfrex2dc  2429  ddifstab  3213  dfss4st  3314  ssddif  3315  difin  3318  difundi  3333  difindiss  3335  indifdir  3337  rabeq0  3397  abeq0  3398  snprc  3596  difprsnss  3666  uni0b  3769  disjnim  3928  brdif  3989  unidif0  4099  dtruex  4482  dcextest  4503  difopab  4680  cnvdif  4953  imadiflem  5210  imadif  5211  brprcneu  5422  poxp  6137  finexdc  6804  snexxph  6846  infmoti  6923  ismkvnex  7037  prltlu  7319  recexprlemdisj  7462  axpre-apti  7717  dfinfre  8738  fzdifsuc  9892  fzp1nel  9915  ntreq0  12340  bj-nnor  13117  bj-nndcALT  13134  nnti  13362