Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3abid Structured version   Visualization version   GIF version

Theorem necon3abid 2818
 Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
Hypothesis
Ref Expression
necon3abid.1 (𝜑 → (𝐴 = 𝐵𝜓))
Assertion
Ref Expression
necon3abid (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))

Proof of Theorem necon3abid
StepHypRef Expression
1 df-ne 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32notbid 307 . 2 (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
41, 3syl5bb 271 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 196  df-ne 2782 This theorem is referenced by:  necon3bbid  2819  necon2abid  2824  foconst  6039  fndmdif  6229  suppsnop  7196  om00el  7543  oeoa  7564  cardsdom2  8697  mulne0b  10547  crne0  10890  expneg  12730  hashsdom  13031  prprrab  13112  gcdn0gt0  15077  cncongr2  15220  pltval3  16790  mulgnegnn  17374  drngmulne0  18592  lvecvsn0  18930  domnmuln0  19119  mvrf1  19246  connsub  21034  pthaus  21251  xkohaus  21266  bndth  22565  lebnumlem1  22568  dvcobr  23515  dvcnvlem  23543  mdegle0  23641  coemulhi  23814  vieta1lem1  23869  vieta1lem2  23870  aalioulem2  23892  cosne0  24080  atandm3  24405  wilthlem2  24595  issqf  24662  mumullem2  24706  dchrptlem3  24791  lgseisenlem3  24902  brbtwn2  25585  colinearalg  25590  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  nmlno0lem  27032  nmlnop0iALT  28238  atcvat2i  28630  divnumden2  28951  bnj1542  30181  bnj1253  30339  ptrecube  32579  poimirlem13  32592  llnexchb2  34173  cdlemb3  34912  rencldnfilem  36402  qirropth  36491  binomcxplemfrat  37572  binomcxplemradcnv  37573  odz2prm2pw  40013  vdn0conngrumgrv2  41363  vdgn1frgrv2  41466
 Copyright terms: Public domain W3C validator