ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  notbii Unicode version

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
StepHypRef Expression
1 notbii.1 . 2  |-  ( ph  <->  ps )
2 notbi 656 . 2  |-  ( (
ph 
<->  ps )  ->  ( -.  ph  <->  -.  ps )
)
31, 2ax-mp 5 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
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  837  xorcom  1367  xordidc  1378  sbn  1926  neirr  2318  dfrex2dc  2429  ddifstab  3212  dfss4st  3313  ssddif  3314  difin  3317  difundi  3332  difindiss  3334  indifdir  3336  rabeq0  3396  abeq0  3397  snprc  3595  difprsnss  3665  uni0b  3768  disjnim  3927  brdif  3988  unidif0  4098  dtruex  4481  dcextest  4502  difopab  4679  cnvdif  4952  imadiflem  5209  imadif  5210  brprcneu  5421  poxp  6136  finexdc  6803  snexxph  6845  infmoti  6922  ismkvnex  7036  prltlu  7318  recexprlemdisj  7461  axpre-apti  7716  dfinfre  8737  fzdifsuc  9891  fzp1nel  9914  ntreq0  12338  bj-nnor  13115  bj-nndcALT  13132  nnti  13360
  Copyright terms: Public domain W3C validator