Theorem notbii 668

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 666	. 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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  678  xchnxbi  680  xchbinx  682  nndc  851  xorcom  1388  xordidc  1399  sbn  1952  neirr  2356  dfrex2dc  2468  ddifstab  3267  dfss4st  3368  ssddif  3369  difin  3372  difundi  3387  difindiss  3389  indifdir  3391  rabeq0  3452  abeq0  3453  snprc  3657  difprsnss  3730  uni0b  3833  disjnim  3992  brdif  4054  unidif0  4165  dtruex  4556  dcextest  4578  difopab  4757  cnvdif  5032  imadiflem  5292  imadif  5293  brprcneu  5505  poxp  6228  finexdc  6897  snexxph  6944  infmoti  7022  ismkvnex  7148  pw1nel3  7225  onntri35  7231  netap  7248  prltlu  7481  recexprlemdisj  7624  axpre-apti  7879  dfinfre  8907  fzdifsuc  10074  fzp1nel  10097  ntreq0  13414  bj-nnor  14257  bj-nndcALT  14281  nnti  14515