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  3295  dfss4st  3396  ssddif  3397  difin  3400  difundi  3415  difindiss  3417  indifdir  3419  rabeq0  3480  abeq0  3481  snprc  3687  difprsnss  3760  uni0b  3864  disjnim  4024  brdif  4086  unidif0  4200  dtruex  4595  dcextest  4617  difopab  4799  cnvdif  5076  imadiflem  5337  imadif  5338  brprcneu  5551  poxp  6290  finexdc  6963  snexxph  7016  infmoti  7094  ismkvnex  7221  pw1nel3  7298  onntri35  7304  netap  7321  prltlu  7554  recexprlemdisj  7697  axpre-apti  7952  dfinfre  8983  fzdifsuc  10156  fzp1nel  10179  ntreq0  14368  bj-nnor  15380  bj-nndcALT  15404  nnti  15639