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  1377  xordidc  1388  sbn  1939  neirr  2343  dfrex2dc  2455  ddifstab  3249  dfss4st  3350  ssddif  3351  difin  3354  difundi  3369  difindiss  3371  indifdir  3373  rabeq0  3433  abeq0  3434  snprc  3635  difprsnss  3705  uni0b  3808  disjnim  3967  brdif  4029  unidif0  4140  dtruex  4530  dcextest  4552  difopab  4731  cnvdif  5004  imadiflem  5261  imadif  5262  brprcneu  5473  poxp  6191  finexdc  6859  snexxph  6906  infmoti  6984  ismkvnex  7110  pw1nel3  7178  onntri35  7184  prltlu  7419  recexprlemdisj  7562  axpre-apti  7817  dfinfre  8842  fzdifsuc  10006  fzp1nel  10029  ntreq0  12673  bj-nnor  13452  bj-nndcALT  13472  nnti  13708