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  3444  abeq0  3445  snprc  3648  difprsnss  3718  uni0b  3821  disjnim  3980  brdif  4042  unidif0  4153  dtruex  4543  dcextest  4565  difopab  4744  cnvdif  5017  imadiflem  5277  imadif  5278  brprcneu  5489  poxp  6211  finexdc  6880  snexxph  6927  infmoti  7005  ismkvnex  7131  pw1nel3  7208  onntri35  7214  prltlu  7449  recexprlemdisj  7592  axpre-apti  7847  dfinfre  8872  fzdifsuc  10037  fzp1nel  10060  ntreq0  12926  bj-nnor  13769  bj-nndcALT  13793  nnti  14027