Theorem notbii 670

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 668	. 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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  680  xchnxbi  682  xchbinx  684  nndc  853  xorcom  1408  xordidc  1419  dcfromnotnotr  1467  dcfromcon  1468  sbn  1980  neirr  2385  dfrex2dc  2497  ddifstab  3305  dfss4st  3406  ssddif  3407  difin  3410  difundi  3425  difindiss  3427  indifdir  3429  rabeq0  3490  abeq0  3491  snprc  3698  difprsnss  3771  uni0b  3875  disjnim  4035  brdif  4098  unidif0  4212  dtruex  4608  dcextest  4630  difopab  4812  cnvdif  5090  imadiflem  5354  imadif  5355  brprcneu  5571  poxp  6320  finexdc  7001  snexxph  7054  infmoti  7132  ismkvnex  7259  pw1nel3  7345  onntri35  7351  netap  7368  prltlu  7602  recexprlemdisj  7745  axpre-apti  8000  dfinfre  9031  fzdifsuc  10205  fzp1nel  10228  ntreq0  14637  bj-nnor  15707  bj-nndcALT  15731  nnti  15966