Theorem notbii 594

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 592	. 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  603  xchnxbi  605  xchbinx  607  dcbii  747  xorcom  1279  xordidc  1290  sbn  1826  neirr  2213  ssddif  3168  difin  3171  difundi  3186  difindiss  3188  indifdir  3190  rabeq0  3244  abeq0  3245  snprc  3432  difprsnss  3499  uni0b  3602  brdif  3809  unidif0  3917  dtruex  4268  difopab  4447  cnvdif  4708  imadiflem  4956  imadif  4957  brprcneu  5149  poxp  5831  prltlu  6557  recexprlemdisj  6700  axpre-apti  6931  fzdifsuc  8901  fzp1nel  8924  nndc  9764