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  684  xchnxbi  686  xchbinx  688  nndc  858  xorcom  1432  xordidc  1443  dcfromnotnotr  1492  dcfromcon  1493  sbn  2005  neirr  2411  dfrex2dc  2523  ddifstab  3339  dfss4st  3440  ssddif  3441  difin  3444  difundi  3459  difindiss  3461  indifdir  3463  rabeq0  3524  abeq0  3525  snprc  3734  difprsnss  3811  uni0b  3918  disjnim  4078  brdif  4142  unidif0  4257  dtruex  4657  dcextest  4679  difopab  4863  cnvdif  5143  imadiflem  5409  imadif  5410  brprcneu  5632  poxp  6397  finexdc  7092  snexxph  7149  infmoti  7227  ismkvnex  7354  pw1nel3  7449  onntri35  7455  netap  7473  prltlu  7707  recexprlemdisj  7850  axpre-apti  8105  dfinfre  9136  fzdifsuc  10316  fzp1nel  10339  swrdccatin2  11310  ntreq0  14858  bj-nnor  16333  bj-nndcALT  16357  nnti  16594