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

Theorem notbii 635
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 633 . 2  |-  ( (
ph 
<->  ps )  ->  ( -.  ph  <->  -.  ps )
)
41, 3ax-mp 7 1  |-  ( -. 
ph 
<->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylnbi  644  xchnxbi  646  xchbinx  648  dcbii  791  xorcom  1334  xordidc  1345  sbn  1886  neirr  2276  dfrex2dc  2387  ddifstab  3155  dfss4st  3256  ssddif  3257  difin  3260  difundi  3275  difindiss  3277  indifdir  3279  rabeq0  3339  abeq0  3340  snprc  3535  difprsnss  3605  uni0b  3708  disjnim  3866  brdif  3923  unidif0  4031  dtruex  4412  dcextest  4433  difopab  4610  cnvdif  4881  imadiflem  5138  imadif  5139  brprcneu  5346  poxp  6059  finexdc  6725  snexxph  6766  infmoti  6830  prltlu  7196  recexprlemdisj  7339  axpre-apti  7570  dfinfre  8572  fzdifsuc  9702  fzp1nel  9725  ntreq0  12083  nndc  12549  nnti  12776
  Copyright terms: Public domain W3C validator