Theorem notbii 674

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 672	. 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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  685  xchnxbi  687  xchbinx  689  nndc  859  xorcom  1433  xordidc  1444  dcfromnotnotr  1493  dcfromcon  1494  sbn  2006  neirr  2421  dfrex2dc  2533  ddifstab  3350  dfss4st  3453  ssddif  3454  difin  3457  difundi  3472  difindiss  3474  indifdir  3476  rabeq0  3537  abeq0  3538  snprc  3753  difprsnss  3831  uni0b  3938  disjnim  4098  brdif  4162  unidif0  4279  dtruex  4680  dcextest  4702  difopab  4887  cnvdif  5168  imadiflem  5434  imadif  5435  brprcneu  5662  poxp  6427  finexdc  7159  snexxph  7219  infmoti  7318  ismkvnex  7445  pw1nel3  7540  onntri35  7546  netap  7564  prltlu  7798  recexprlemdisj  7941  axpre-apti  8196  dfinfre  9226  fzdifsuc  10411  fzp1nel  10434  swrdccatin2  11414  ntreq0  14984  bj-nnor  16493  bj-nndcALT  16517  nnti  16753