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  684  xchnxbi  686  xchbinx  688  nndc  858  xorcom  1432  xordidc  1443  dcfromnotnotr  1492  dcfromcon  1493  sbn  2004  neirr  2410  dfrex2dc  2522  ddifstab  3338  dfss4st  3439  ssddif  3440  difin  3443  difundi  3458  difindiss  3460  indifdir  3462  rabeq0  3523  abeq0  3524  snprc  3735  difprsnss  3812  uni0b  3919  disjnim  4079  brdif  4143  unidif0  4259  dtruex  4659  dcextest  4681  difopab  4865  cnvdif  5145  imadiflem  5411  imadif  5412  brprcneu  5635  poxp  6402  finexdc  7097  snexxph  7154  infmoti  7232  ismkvnex  7359  pw1nel3  7454  onntri35  7460  netap  7478  prltlu  7712  recexprlemdisj  7855  axpre-apti  8110  dfinfre  9141  fzdifsuc  10321  fzp1nel  10344  swrdccatin2  11319  ntreq0  14885  bj-nnor  16391  bj-nndcALT  16415  nnti  16651