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  2008  neirr  2423  dfrex2dc  2535  ddifstab  3355  dfss4st  3458  ssddif  3459  difin  3462  difundi  3477  difindiss  3479  indifdir  3481  rabeq0  3542  abeq0  3543  snprc  3759  difprsnss  3837  uni0b  3944  disjnim  4104  brdif  4168  unidif0  4285  dtruex  4686  dcextest  4708  difopab  4893  cnvdif  5174  imadiflem  5440  imadif  5441  brprcneu  5668  poxp  6441  finexdc  7173  snexxph  7233  infmoti  7332  ismkvnex  7459  pw1nel3  7554  onntri35  7560  netap  7584  prltlu  7818  recexprlemdisj  7961  axpre-apti  8216  dfinfre  9247  fzdifsuc  10437  fzp1nel  10460  swrdccatin2  11446  ntreq0  15123  bj-nnor  16632  bj-nndcALT  16656  nnti  16892