Theorem notbii 593

Description: Negate both sides of a logical equivalence. (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		id 19	. . 3 ⊢ ((φ ↔ ψ) → (φ ↔ ψ))
3	2	notbid 591	. 2 ⊢ ((φ ↔ ψ) → (¬ φ ↔ ¬ ψ))
4	1, 3	ax-mp 7	1 ⊢ (¬ φ ↔ ¬ ψ)

Syntax hints:  ¬ wn 3   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sylnbi  602  xchnxbi  604  xchbinx  606  dcbii  746  xorcom  1276  xordidc  1287  sbn  1823  neirr  2210  ssddif  3165  difin  3168  difundi  3183  difindiss  3185  indifdir  3187  rabeq0  3241  abeq0  3242  snprc  3426  difprsnss  3493  uni0b  3596  brdif  3803  unidif0  3911  dtruex  4237  difopab  4412  cnvdif  4673  imadiflem  4921  imadif  4922  brprcneu  5114  poxp  5794  prltlu  6470  recexprlemdisj  6602  axpre-apti  6769  fzdifsuc  8713  fzp1nel  8736  nndc  9235