Theorem notbii 669

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 667	. 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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  679  xchnxbi  681  xchbinx  683  nndc  852  xorcom  1399  xordidc  1410  dcfromnotnotr  1458  dcfromcon  1459  sbn  1971  neirr  2376  dfrex2dc  2488  ddifstab  3296  dfss4st  3397  ssddif  3398  difin  3401  difundi  3416  difindiss  3418  indifdir  3420  rabeq0  3481  abeq0  3482  snprc  3688  difprsnss  3761  uni0b  3865  disjnim  4025  brdif  4087  unidif0  4201  dtruex  4596  dcextest  4618  difopab  4800  cnvdif  5077  imadiflem  5338  imadif  5339  brprcneu  5554  poxp  6299  finexdc  6972  snexxph  7025  infmoti  7103  ismkvnex  7230  pw1nel3  7314  onntri35  7320  netap  7337  prltlu  7571  recexprlemdisj  7714  axpre-apti  7969  dfinfre  9000  fzdifsuc  10173  fzp1nel  10196  ntreq0  14452  bj-nnor  15464  bj-nndcALT  15488  nnti  15723