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

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
StepHypRef Expression
1 notbii.1 . 2  |-  ( ph  <->  ps )
2 id 19 . . 3  |-  ( (
ph 
<->  ps )  ->  ( ph 
<->  ps ) )
32notbid 625 . 2  |-  ( (
ph 
<->  ps )  ->  ( -.  ph  <->  -.  ps )
)
41, 3ax-mp 7 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
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  783  xorcom  1322  xordidc  1333  sbn  1871  neirr  2260  dfrex2dc  2367  ddifstab  3121  dfss4st  3221  ssddif  3222  difin  3225  difundi  3240  difindiss  3242  indifdir  3244  rabeq0  3301  abeq0  3302  snprc  3490  difprsnss  3558  uni0b  3661  brdif  3868  unidif0  3977  dtruex  4348  dcextest  4369  difopab  4537  cnvdif  4804  imadiflem  5058  imadif  5059  brprcneu  5261  poxp  5954  finexdc  6570  snexxph  6608  infmoti  6667  prltlu  6990  recexprlemdisj  7133  axpre-apti  7364  dfinfre  8352  fzdifsuc  9425  fzp1nel  9448  nndc  11099  nnti  11330
  Copyright terms: Public domain W3C validator