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

Theorem necon3abid 3050
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 3015 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3abid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32notbid 320 . 2 (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
41, 3syl5bb 285 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208   = wceq 1530  wne 3014
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 209  df-ne 3015
This theorem is referenced by:  necon3bbid  3051  necon2abid  3056  prnesn  4782  foconst  6596  fndmdif  6805  suppsnop  7836  om00el  8194  oeoa  8215  cardsdom2  9409  mulne0b  11273  crne0  11623  expneg  13429  hashsdom  13734  prprrab  13823  gcdn0gt0  15858  cncongr2  16004  pltval3  17569  mulgnegnn  18230  drngmulne0  19516  lvecvsn0  19873  domnmuln0  20063  mvrf1  20197  connsub  22021  pthaus  22238  xkohaus  22253  bndth  23554  lebnumlem1  23557  dvcobr  24535  dvcnvlem  24565  mdegle0  24663  coemulhi  24836  vieta1lem1  24891  vieta1lem2  24892  aalioulem2  24914  cosne0  25106  atandm3  25448  wilthlem2  25638  issqf  25705  mumullem2  25749  dchrptlem3  25834  lgseisenlem3  25945  brbtwn2  26683  colinearalg  26688  vdn0conngrumgrv2  27967  vdgn1frgrv2  28067  nmlno0lem  28562  nmlnop0iALT  29764  atcvat2i  30156  divnumden2  30526  lindssn  30932  fedgmullem2  31014  bnj1542  32117  bnj1253  32277  ptrecube  34879  poimirlem13  34892  ecinn0  35594  llnexchb2  36992  cdlemb3  37729  rencldnfilem  39402  qirropth  39490  binomcxplemfrat  40668  binomcxplemradcnv  40669  odz2prm2pw  43710
  Copyright terms: Public domain W3C validator