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  2215  ssddif  3171  difin  3174  difundi  3189  difindiss  3191  indifdir  3193  rabeq0  3247  abeq0  3248  snprc  3435  difprsnss  3502  uni0b  3605  brdif  3812  unidif0  3920  dtruex  4283  difopab  4469  cnvdif  4730  imadiflem  4978  imadif  4979  brprcneu  5171  poxp  5853  prltlu  6585  recexprlemdisj  6728  axpre-apti  6959  fzdifsuc  8943  fzp1nel  8966  nndc  9900