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  1968  neirr  2373  dfrex2dc  2485  ddifstab  3291  dfss4st  3392  ssddif  3393  difin  3396  difundi  3411  difindiss  3413  indifdir  3415  rabeq0  3476  abeq0  3477  snprc  3683  difprsnss  3756  uni0b  3860  disjnim  4020  brdif  4082  unidif0  4196  dtruex  4591  dcextest  4613  difopab  4795  cnvdif  5072  imadiflem  5333  imadif  5334  brprcneu  5547  poxp  6285  finexdc  6958  snexxph  7009  infmoti  7087  ismkvnex  7214  pw1nel3  7291  onntri35  7297  netap  7314  prltlu  7547  recexprlemdisj  7690  axpre-apti  7945  dfinfre  8975  fzdifsuc  10147  fzp1nel  10170  ntreq0  14300  bj-nnor  15226  bj-nndcALT  15250  nnti  15485