Theorem notbii 670

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 668	. 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  680  xchnxbi  682  xchbinx  684  nndc  853  xorcom  1408  xordidc  1419  dcfromnotnotr  1467  dcfromcon  1468  sbn  1980  neirr  2385  dfrex2dc  2497  ddifstab  3305  dfss4st  3406  ssddif  3407  difin  3410  difundi  3425  difindiss  3427  indifdir  3429  rabeq0  3490  abeq0  3491  snprc  3698  difprsnss  3771  uni0b  3875  disjnim  4035  brdif  4097  unidif0  4211  dtruex  4607  dcextest  4629  difopab  4811  cnvdif  5089  imadiflem  5353  imadif  5354  brprcneu  5569  poxp  6318  finexdc  6999  snexxph  7052  infmoti  7130  ismkvnex  7257  pw1nel3  7343  onntri35  7349  netap  7366  prltlu  7600  recexprlemdisj  7743  axpre-apti  7998  dfinfre  9029  fzdifsuc  10203  fzp1nel  10226  ntreq0  14604  bj-nnor  15670  bj-nndcALT  15694  nnti  15929