Theorem notbii 669

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 667	. 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  679  xchnxbi  681  xchbinx  683  nndc  852  xorcom  1407  xordidc  1418  dcfromnotnotr  1466  dcfromcon  1467  sbn  1979  neirr  2384  dfrex2dc  2496  ddifstab  3304  dfss4st  3405  ssddif  3406  difin  3409  difundi  3424  difindiss  3426  indifdir  3428  rabeq0  3489  abeq0  3490  snprc  3697  difprsnss  3770  uni0b  3874  disjnim  4034  brdif  4096  unidif0  4210  dtruex  4606  dcextest  4628  difopab  4810  cnvdif  5088  imadiflem  5352  imadif  5353  brprcneu  5568  poxp  6317  finexdc  6998  snexxph  7051  infmoti  7129  ismkvnex  7256  pw1nel3  7342  onntri35  7348  netap  7365  prltlu  7599  recexprlemdisj  7742  axpre-apti  7997  dfinfre  9028  fzdifsuc  10202  fzp1nel  10225  ntreq0  14575  bj-nnor  15632  bj-nndcALT  15656  nnti  15891