Theorem notbii 678

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylnbi  689  xchnxbi  691  xchbinx  693  nndc  863  xorcom  1437  xordidc  1448  dcfromnotnotr  1497  dcfromcon  1498  sbn  2012  neirr  2429  dfrex2dc  2541  ddifstab  3361  dfss4st  3464  ssddif  3465  difin  3468  difundi  3483  difindiss  3485  indifdir  3487  rabeq0  3552  abeq0  3553  snprc  3774  difprsnss  3853  uni0b  3960  disjnim  4120  brdif  4184  unidif0  4304  dtruex  4706  dcextest  4728  difopab  4913  cnvdif  5194  imadiflem  5460  imadif  5461  brprcneu  5688  poxp  6468  finexdc  7207  snexxph  7267  infmoti  7368  ismkvnex  7495  pw1nel3  7590  onntri35  7596  netap  7620  prltlu  7854  recexprlemdisj  7997  axpre-apti  8252  dfinfre  9286  fzdifsuc  10488  fzp1nel  10511  swrdccatin2  11501  ntreq0  15233  bj-nnor  16762  bj-nndcALT  16786  nnti  17022  wexmiddc  17042