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  3444  abeq0  3445  snprc  3648  difprsnss  3718  uni0b  3821  disjnim  3980  brdif  4042  unidif0  4153  dtruex  4543  dcextest  4565  difopab  4744  cnvdif  5017  imadiflem  5277  imadif  5278  brprcneu  5489  poxp  6211  finexdc  6880  snexxph  6927  infmoti  7005  ismkvnex  7131  pw1nel3  7208  onntri35  7214  prltlu  7449  recexprlemdisj  7592  axpre-apti  7847  dfinfre  8872  fzdifsuc  10037  fzp1nel  10060  ntreq0  12926  bj-nnor  13769  bj-nndcALT  13793  nnti  14027
  Copyright terms: Public domain W3C validator