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

Theorem notbii 594
 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
Assertion
Ref Expression
notbii

Proof of Theorem notbii
StepHypRef Expression
1 notbii.1 . 2
2 id 19 . . 3
32notbid 592 . 2
41, 3ax-mp 7 1
 Colors of variables: wff set class Syntax hints:   wn 3   wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  sylnbi  603  xchnxbi  605  xchbinx  607  dcbii  747  xorcom  1279  xordidc  1290  sbn  1826  neirr  2215  ssddif  3171  difin  3174  difundi  3189  difindiss  3191  indifdir  3193  rabeq0  3247  abeq0  3248  snprc  3435  difprsnss  3502  uni0b  3605  brdif  3812  unidif0  3920  dtruex  4283  difopab  4469  cnvdif  4730  imadiflem  4978  imadif  4979  brprcneu  5171  poxp  5853  prltlu  6585  recexprlemdisj  6728  axpre-apti  6959  fzdifsuc  8943  fzp1nel  8966  nndc  9900
 Copyright terms: Public domain W3C validator