Theorem notbii 663

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 661	. 2 |- ( ( ph <-> ps ) -> ( -. ph <-> -. ps ) )
3	1, 2	ax-mp 5	1 |- ( -. ph <-> -. ps )

Syntax hints:   -. wn 3   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnbi  673  xchnxbi  675  xchbinx  677  nndc  846  xorcom  1383  xordidc  1394  sbn  1945  neirr  2349  dfrex2dc  2461  ddifstab  3259  dfss4st  3360  ssddif  3361  difin  3364  difundi  3379  difindiss  3381  indifdir  3383  rabeq0  3443  abeq0  3444  snprc  3646  difprsnss  3716  uni0b  3819  disjnim  3978  brdif  4040  unidif0  4151  dtruex  4541  dcextest  4563  difopab  4742  cnvdif  5015  imadiflem  5275  imadif  5276  brprcneu  5487  poxp  6209  finexdc  6878  snexxph  6925  infmoti  7003  ismkvnex  7129  pw1nel3  7201  onntri35  7207  prltlu  7442  recexprlemdisj  7585  axpre-apti  7840  dfinfre  8865  fzdifsuc  10030  fzp1nel  10053  ntreq0  12891  bj-nnor  13734  bj-nndcALT  13758  nnti  13992