Theorem notbii 627

Description: Negate both sides of a logical equivalence. (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		id 19	. . 3 |- ( ( ph <-> ps ) -> ( ph <-> ps ) )
3	2	notbid 625	. 2 |- ( ( ph <-> ps ) -> ( -. ph <-> -. ps ) )
4	1, 3	ax-mp 7	1 |- ( -. ph <-> -. ps )

Syntax hints:   -. wn 3   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylnbi  636  xchnxbi  638  xchbinx  640  dcbii  781  xorcom  1320  xordidc  1331  sbn  1868  neirr  2255  ddifstab  3105  ssddif  3205  difin  3208  difundi  3223  difindiss  3225  indifdir  3227  rabeq0  3281  abeq0  3282  snprc  3465  difprsnss  3532  uni0b  3634  brdif  3841  unidif0  3949  dtruex  4310  difopab  4497  cnvdif  4760  imadiflem  5009  imadif  5010  brprcneu  5202  poxp  5884  infmoti  6500  prltlu  6739  recexprlemdisj  6882  axpre-apti  7113  dfinfre  8101  fzdifsuc  9174  fzp1nel  9197  nndc  10722