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  3336  dfss4st  3437  ssddif  3438  difin  3441  difundi  3456  difindiss  3458  indifdir  3460  rabeq0  3521  abeq0  3522  snprc  3731  difprsnss  3805  uni0b  3912  disjnim  4072  brdif  4136  unidif0  4250  dtruex  4650  dcextest  4672  difopab  4854  cnvdif  5134  imadiflem  5399  imadif  5400  brprcneu  5619  poxp  6376  finexdc  7060  snexxph  7113  infmoti  7191  ismkvnex  7318  pw1nel3  7412  onntri35  7418  netap  7436  prltlu  7670  recexprlemdisj  7813  axpre-apti  8068  dfinfre  9099  fzdifsuc  10273  fzp1nel  10296  swrdccatin2  11256  ntreq0  14800  bj-nnor  16056  bj-nndcALT  16080  nnti  16315