Theorem notbii 672

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 670	. 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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  682  xchnxbi  684  xchbinx  686  nndc  856  xorcom  1430  xordidc  1441  dcfromnotnotr  1490  dcfromcon  1491  sbn  2003  neirr  2409  dfrex2dc  2521  ddifstab  3337  dfss4st  3438  ssddif  3439  difin  3442  difundi  3457  difindiss  3459  indifdir  3461  rabeq0  3522  abeq0  3523  snprc  3732  difprsnss  3809  uni0b  3916  disjnim  4076  brdif  4140  unidif0  4255  dtruex  4655  dcextest  4677  difopab  4861  cnvdif  5141  imadiflem  5406  imadif  5407  brprcneu  5628  poxp  6392  finexdc  7085  snexxph  7140  infmoti  7218  ismkvnex  7345  pw1nel3  7439  onntri35  7445  netap  7463  prltlu  7697  recexprlemdisj  7840  axpre-apti  8095  dfinfre  9126  fzdifsuc  10306  fzp1nel  10329  swrdccatin2  11300  ntreq0  14846  bj-nnor  16266  bj-nndcALT  16290  nnti  16527