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

Theorem necon3abid 3052
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 3017 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32notbid 319 . 2 (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
41, 3syl5bb 284 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon3bbid  3053  necon2abid  3058  prnesn  4784  foconst  6597  fndmdif  6805  suppsnop  7835  om00el  8192  oeoa  8213  cardsdom2  9406  mulne0b  11270  crne0  11620  expneg  13427  hashsdom  13732  prprrab  13821  gcdn0gt0  15856  cncongr2  16002  pltval3  17567  mulgnegnn  18178  drngmulne0  19455  lvecvsn0  19812  domnmuln0  20001  mvrf1  20135  connsub  21959  pthaus  22176  xkohaus  22191  bndth  23491  lebnumlem1  23494  dvcobr  24472  dvcnvlem  24502  mdegle0  24600  coemulhi  24773  vieta1lem1  24828  vieta1lem2  24829  aalioulem2  24851  cosne0  25041  atandm3  25383  wilthlem2  25574  issqf  25641  mumullem2  25685  dchrptlem3  25770  lgseisenlem3  25881  brbtwn2  26619  colinearalg  26624  vdn0conngrumgrv2  27903  vdgn1frgrv2  28003  nmlno0lem  28498  nmlnop0iALT  29700  atcvat2i  30092  divnumden2  30461  lindssn  30867  fedgmullem2  30926  bnj1542  32029  bnj1253  32187  ptrecube  34774  poimirlem13  34787  ecinn0  35490  llnexchb2  36887  cdlemb3  37624  rencldnfilem  39297  qirropth  39385  binomcxplemfrat  40563  binomcxplemradcnv  40564  odz2prm2pw  43572
  Copyright terms: Public domain W3C validator