Theorem notbii 635

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 633	. 2 |- ( ( ph <-> ps ) -> ( -. ph <-> -. ps ) )
4	1, 3	ax-mp 7	1 |- ( -. ph <-> -. ps )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnbi  644  xchnxbi  646  xchbinx  648  dcbii  791  xorcom  1334  xordidc  1345  sbn  1886  neirr  2276  dfrex2dc  2387  ddifstab  3155  dfss4st  3256  ssddif  3257  difin  3260  difundi  3275  difindiss  3277  indifdir  3279  rabeq0  3339  abeq0  3340  snprc  3535  difprsnss  3605  uni0b  3708  disjnim  3866  brdif  3923  unidif0  4031  dtruex  4412  dcextest  4433  difopab  4610  cnvdif  4881  imadiflem  5138  imadif  5139  brprcneu  5346  poxp  6059  finexdc  6725  snexxph  6766  infmoti  6830  prltlu  7196  recexprlemdisj  7339  axpre-apti  7570  dfinfre  8572  fzdifsuc  9702  fzp1nel  9725  ntreq0  12083  nndc  12549  nnti  12776