Theorem notbii 678

Description: Equivalence property for negation. Inference form. (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		notbi 676	. 2 |- ( ( ph <-> ps ) -> ( -. ph <-> -. ps ) )
3	1, 2	ax-mp 5	1 |- ( -. ph <-> -. ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  689  xchnxbi  691  xchbinx  693  nndc  863  xorcom  1437  xordidc  1448  dcfromnotnotr  1497  dcfromcon  1498  sbn  2012  neirr  2429  dfrex2dc  2541  ddifstab  3361  dfss4st  3464  ssddif  3465  difin  3468  difundi  3483  difindiss  3485  indifdir  3487  rabeq0  3552  abeq0  3553  snprc  3773  difprsnss  3851  uni0b  3958  disjnim  4118  brdif  4182  unidif0  4302  dtruex  4704  dcextest  4726  difopab  4911  cnvdif  5192  imadiflem  5458  imadif  5459  brprcneu  5686  poxp  6462  finexdc  7201  snexxph  7261  infmoti  7362  ismkvnex  7489  pw1nel3  7584  onntri35  7590  netap  7614  prltlu  7848  recexprlemdisj  7991  axpre-apti  8246  dfinfre  9280  fzdifsuc  10471  fzp1nel  10494  swrdccatin2  11484  ntreq0  15216  bj-nnor  16745  bj-nndcALT  16769  nnti  17005