Theorem notbii 626

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	|- ( ph <-> ps )

Assertion

Ref	Expression
notbii	|- ( -. ph <-> -. ps )

Proof of Theorem notbii

Step	Hyp	Ref	Expression
1		notbii.1	. 2 |- ( ph <-> ps )
2		id 19	. . 3 |- ( ( ph <-> ps ) -> ( ph <-> ps ) )
3	2	notbid 624	. 2 |- ( ( ph <-> ps ) -> ( -. ph <-> -. ps ) )
4	1, 3	ax-mp 7	1 |- ( -. ph <-> -. ps )

Syntax hints:   -. wn 3   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylnbi  635  xchnxbi  637  xchbinx  639  dcbii  780  xorcom  1319  xordidc  1330  sbn  1867  neirr  2254  ddifstab  3104  ssddif  3198  difin  3201  difundi  3216  difindiss  3218  indifdir  3220  rabeq0  3274  abeq0  3275  snprc  3457  difprsnss  3524  uni0b  3626  brdif  3833  unidif0  3941  dtruex  4302  difopab  4487  cnvdif  4750  imadiflem  4998  imadif  4999  brprcneu  5191  poxp  5873  infmoti  6441  prltlu  6677  recexprlemdisj  6820  axpre-apti  7051  dfinfre  8034  fzdifsuc  9098  fzp1nel  9121  nndc  10571