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 )

This proof depends on syntax axioms:   -. wn 3   <-> wb 105

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  3774  difprsnss  3853  uni0b  3960  disjnim  4120  brdif  4184  unidif0  4304  dtruex  4706  dcextest  4728  difopab  4913  cnvdif  5194  imadiflem  5460  imadif  5461  brprcneu  5688  poxp  6468  finexdc  7207  snexxph  7267  infmoti  7369  ismkvnex  7496  pw1nel3  7591  onntri35  7597  netap  7621  prltlu  7855  recexprlemdisj  7998  axpre-apti  8253  dfinfre  9289  fzdifsuc  10499  fzp1nel  10522  swrdccatin2  11516  ntreq0  15285  bj-nnor  16884  bj-nndcALT  16908  nnti  17144  wexmiddc  17164