Theorem notbii 658

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 656	. 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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnbi  668  xchnxbi  670  xchbinx  672  nndc  841  xorcom  1378  xordidc  1389  sbn  1940  neirr  2345  dfrex2dc  2457  ddifstab  3254  dfss4st  3355  ssddif  3356  difin  3359  difundi  3374  difindiss  3376  indifdir  3378  rabeq0  3438  abeq0  3439  snprc  3641  difprsnss  3711  uni0b  3814  disjnim  3973  brdif  4035  unidif0  4146  dtruex  4536  dcextest  4558  difopab  4737  cnvdif  5010  imadiflem  5267  imadif  5268  brprcneu  5479  poxp  6200  finexdc  6868  snexxph  6915  infmoti  6993  ismkvnex  7119  pw1nel3  7187  onntri35  7193  prltlu  7428  recexprlemdisj  7571  axpre-apti  7826  dfinfre  8851  fzdifsuc  10016  fzp1nel  10039  ntreq0  12782  bj-nnor  13625  bj-nndcALT  13649  nnti  13884