Theorem notbii 668

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 666	. 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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnbi  678  xchnxbi  680  xchbinx  682  nndc  851  xorcom  1388  xordidc  1399  sbn  1952  neirr  2356  dfrex2dc  2468  ddifstab  3268  dfss4st  3369  ssddif  3370  difin  3373  difundi  3388  difindiss  3390  indifdir  3392  rabeq0  3453  abeq0  3454  snprc  3658  difprsnss  3731  uni0b  3835  disjnim  3995  brdif  4057  unidif0  4168  dtruex  4559  dcextest  4581  difopab  4761  cnvdif  5036  imadiflem  5296  imadif  5297  brprcneu  5509  poxp  6233  finexdc  6902  snexxph  6949  infmoti  7027  ismkvnex  7153  pw1nel3  7230  onntri35  7236  netap  7253  prltlu  7486  recexprlemdisj  7629  axpre-apti  7884  dfinfre  8913  fzdifsuc  10081  fzp1nel  10104  ntreq0  13635  bj-nnor  14489  bj-nndcALT  14513  nnti  14747