Theorem notbii 678

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

This proof depends on syntax axioms:   -. wn 3   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylnbi  689  xchnxbi  691  xchbinx  693  nndc  863  xorcom  1437  xordidc  1448  dcfromnotnotr  1497  dcfromcon  1498  sbn  2012  neirr  2429  dfrex2dc  2541  ddifstab  3361  dfss4st  3464  ssddif  3465  difin  3468  difundi  3483  difindiss  3485  indifdir  3487  rabeq0  3552  abeq0  3553  snprc  3774  difprsnss  3853  uni0b  3960  disjnim  4120  brdif  4185  unidif0  4306  dtruex  4708  dcextest  4730  difopab  4915  cnvdif  5197  imadiflem  5463  imadif  5464  brprcneu  5691  poxp  6472  finexdc  7212  snexxph  7273  infmoti  7375  ismkvnex  7502  pw1nel3  7597  onntri35  7603  netap  7627  prltlu  7861  recexprlemdisj  8004  axpre-apti  8259  dfinfre  9295  fzdifsuc  10506  fzp1nel  10529  swrdccatin2  11524  ntreq0  15370  bj-nnor  16979  bj-nndcALT  17003  nnti  17239  wexmiddc  17259