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  781  xorcom  1320  xordidc  1331  sbn  1868  neirr  2255  ddifstab  3105  ssddif  3205  difin  3208  difundi  3223  difindiss  3225  indifdir  3227  rabeq0  3281  abeq0  3282  snprc  3465  difprsnss  3532  uni0b  3634  brdif  3841  unidif0  3949  dtruex  4310  difopab  4497  cnvdif  4760  imadiflem  5009  imadif  5010  brprcneu  5202  poxp  5884  infmoti  6500  prltlu  6739  recexprlemdisj  6882  axpre-apti  7113  dfinfre  8101  fzdifsuc  9174  fzp1nel  9197  nndc  10722
  Copyright terms: Public domain W3C validator