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

Theorem necon3abid 2977
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 2941 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32notbid 318 . 2 (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
41, 3bitrid 283 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1542  wne 2940
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 206  df-ne 2941
This theorem is referenced by:  necon3bbid  2978  necon2abid  2983  prnesn  4818  foconst  6772  fndmdif  6993  suppsnop  8110  om00el  8524  oeoa  8545  cardsdom2  9929  mulne0b  11801  crne0  12151  expneg  13981  hashsdom  14287  prprrab  14378  gcdn0gt0  16403  cncongr2  16549  pltval3  18233  mulgnegnn  18891  drngmulne0  20223  lvecvsn0  20586  domnmuln0  20784  mvrf1  21410  connsub  22788  pthaus  23005  xkohaus  23020  bndth  24337  lebnumlem1  24340  dvcobr  25326  dvcnvlem  25356  mdegle0  25458  coemulhi  25631  vieta1lem1  25686  vieta1lem2  25687  aalioulem2  25709  cosne0  25901  atandm3  26244  wilthlem2  26434  issqf  26501  mumullem2  26545  dchrptlem3  26630  lgseisenlem3  26741  brbtwn2  27896  colinearalg  27901  vdn0conngrumgrv2  29182  vdgn1frgrv2  29282  nmlno0lem  29777  nmlnop0iALT  30979  atcvat2i  31371  divnumden2  31763  lindssn  32213  fedgmullem2  32382  bnj1542  33526  bnj1253  33686  ptrecube  36124  poimirlem13  36137  ecinn0  36860  llnexchb2  38378  cdlemb3  39115  aks6d1c2p2  40595  fsuppind  40808  rencldnfilem  41186  qirropth  41274  binomcxplemfrat  42719  binomcxplemradcnv  42720  odz2prm2pw  45841
  Copyright terms: Public domain W3C validator