Theorem notbii 668

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 666	. 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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  678  xchnxbi  680  xchbinx  682  nndc  851  xorcom  1388  xordidc  1399  sbn  1952  neirr  2356  dfrex2dc  2468  ddifstab  3269  dfss4st  3370  ssddif  3371  difin  3374  difundi  3389  difindiss  3391  indifdir  3393  rabeq0  3454  abeq0  3455  snprc  3659  difprsnss  3732  uni0b  3836  disjnim  3996  brdif  4058  unidif0  4169  dtruex  4560  dcextest  4582  difopab  4762  cnvdif  5037  imadiflem  5297  imadif  5298  brprcneu  5510  poxp  6235  finexdc  6904  snexxph  6951  infmoti  7029  ismkvnex  7155  pw1nel3  7232  onntri35  7238  netap  7255  prltlu  7488  recexprlemdisj  7631  axpre-apti  7886  dfinfre  8915  fzdifsuc  10083  fzp1nel  10106  ntreq0  13671  bj-nnor  14525  bj-nndcALT  14549  nnti  14783