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

Theorem notbid 591
Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
Hypothesis
Ref Expression
notbid.1
Assertion
Ref Expression
notbid

Proof of Theorem notbid
StepHypRef Expression
1 notbid.1 . . . 4
21biimprd 147 . . 3
32con3d 560 . 2
41biimpd 132 . . 3
54con3d 560 . 2
63, 5impbid 120 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   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:  notbii  593  dcbid  747  con1biidc  770  pm4.54dc  804  xorbi2d  1269  xorbi1d  1270  pm5.18im  1273  pm5.24dc  1286  neeq1  2213  neeq2  2214  necon3abid  2238  neleq1  2295  neleq2  2296  cdeqnot  2746  ru  2757  sbcng  2797  sbcnel12g  2861  sbcne12g  2862  difjust  2913  eldif  2921  dfpss3  3024  difeq2  3050  disjne  3267  ifbi  3342  prel12  3533  nalset  3878  pwnss  3903  poeq1  4027  pocl  4031  swopo  4034  sotritrieq  4053  regexmidlem1  4218  regexmid  4219  nlimsucg  4242  nndceq0  4282  nnregexmid  4285  poinxp  4352  posng  4355  intirr  4654  poirr2  4660  cnvpom  4803  fndmdif  5215  f1imapss  5358  isopolem  5404  poxp  5794  nnmword  6027  brdifun  6069  swoer  6070  2dom  6221  pitric  6305  addnidpig  6320  ltsonq  6382  elinp  6457  prltlu  6470  prdisj  6475  ltexprlemdisj  6580  ltposr  6691  aptisr  6705  axpre-ltirr  6766  axpre-apti  6769  xrlenlt  6881  axapti  6887  lttri3  6895  ltne  6900  leadd1  7220  reapti  7363  lemul1  7377  apirr  7389  apti  7406  lediv1  7616  lemuldiv  7628  lerec  7631  le2msq  7648  avgle1  7942  avgle2  7943  znnnlt1  8069  eluzdc  8323  qapne  8350  xrltne  8499  xleneg  8520  nn0disj  8765  elfzonelfzo  8856  expeq0  8940  bj-nalset  9348  bj-nnelirr  9411
  Copyright terms: Public domain W3C validator