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

Theorem notbii 663
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 661 . 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 609  ax-in2 610
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylnbi  673  xchnxbi  675  xchbinx  677  nndc  846  xorcom  1383  xordidc  1394  sbn  1945  neirr  2349  dfrex2dc  2461  ddifstab  3259  dfss4st  3360  ssddif  3361  difin  3364  difundi  3379  difindiss  3381  indifdir  3383  rabeq0  3443  abeq0  3444  snprc  3646  difprsnss  3716  uni0b  3819  disjnim  3978  brdif  4040  unidif0  4151  dtruex  4541  dcextest  4563  difopab  4742  cnvdif  5015  imadiflem  5275  imadif  5276  brprcneu  5487  poxp  6209  finexdc  6878  snexxph  6925  infmoti  7003  ismkvnex  7129  pw1nel3  7201  onntri35  7207  prltlu  7442  recexprlemdisj  7585  axpre-apti  7840  dfinfre  8865  fzdifsuc  10030  fzp1nel  10053  ntreq0  12891  bj-nnor  13734  bj-nndcALT  13758  nnti  13992
  Copyright terms: Public domain W3C validator