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  2004  neirr  2410  dfrex2dc  2522  ddifstab  3338  dfss4st  3439  ssddif  3440  difin  3443  difundi  3458  difindiss  3460  indifdir  3462  rabeq0  3523  abeq0  3524  snprc  3733  difprsnss  3810  uni0b  3917  disjnim  4077  brdif  4141  unidif0  4256  dtruex  4656  dcextest  4678  difopab  4862  cnvdif  5142  imadiflem  5408  imadif  5409  brprcneu  5632  poxp  6399  finexdc  7094  snexxph  7151  infmoti  7229  ismkvnex  7356  pw1nel3  7451  onntri35  7457  netap  7475  prltlu  7709  recexprlemdisj  7852  axpre-apti  8107  dfinfre  9138  fzdifsuc  10318  fzp1nel  10341  swrdccatin2  11316  ntreq0  14882  bj-nnor  16388  bj-nndcALT  16412  nnti  16649