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  685  xchnxbi  687  xchbinx  689  nndc  859  xorcom  1433  xordidc  1444  dcfromnotnotr  1493  dcfromcon  1494  sbn  2008  neirr  2423  dfrex2dc  2535  ddifstab  3353  dfss4st  3456  ssddif  3457  difin  3460  difundi  3475  difindiss  3477  indifdir  3479  rabeq0  3540  abeq0  3541  snprc  3756  difprsnss  3834  uni0b  3941  disjnim  4101  brdif  4165  unidif0  4282  dtruex  4683  dcextest  4705  difopab  4890  cnvdif  5171  imadiflem  5437  imadif  5438  brprcneu  5665  poxp  6430  finexdc  7162  snexxph  7222  infmoti  7321  ismkvnex  7448  pw1nel3  7543  onntri35  7549  netap  7573  prltlu  7807  recexprlemdisj  7950  axpre-apti  8205  dfinfre  9235  fzdifsuc  10422  fzp1nel  10445  swrdccatin2  11429  ntreq0  15046  bj-nnor  16555  bj-nndcALT  16579  nnti  16815