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

Theorem necon3bbid 3024
Description: Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
Hypothesis
Ref Expression
necon3bbid.1 (𝜑 → (𝜓𝐴 = 𝐵))
Assertion
Ref Expression
necon3bbid (𝜑 → (¬ 𝜓𝐴𝐵))

Proof of Theorem necon3bbid
StepHypRef Expression
1 necon3bbid.1 . . . 4 (𝜑 → (𝜓𝐴 = 𝐵))
21bicomd 226 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 3023 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 226 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209   = wceq 1538  wne 2987
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 210  df-ne 2988
This theorem is referenced by:  necon1abid  3025  necon3bid  3031  eldifsn  4680  php  8685  xmullem2  12646  seqcoll2  13819  cnpart  14591  rlimrecl  14929  ncoprmgcdne1b  15984  prmrp  16046  4sqlem17  16287  mrieqvd  16901  mrieqv2d  16902  pltval  17562  latnlemlt  17686  latnle  17687  odnncl  18665  gexnnod  18705  sylow1lem1  18715  slwpss  18729  lssnle  18792  lspsnne1  19882  nzrunit  20033  cnsubrg  20151  psrridm  20642  cmpfi  22013  hausdiag  22250  txhaus  22252  isusp  22867  recld2  23419  metdseq0  23459  i1f1lem  24293  aaliou2b  24937  dvloglem  25239  logf1o2  25241  lgsne0  25919  lgsqr  25935  2sqlem7  26008  ostth3  26222  tglngne  26344  tgelrnln  26424  eucrct2eupth  28030  norm1exi  29033  atnemeq0  30160  opeldifid  30362  pridln1  31026  mxidln1  31046  ssmxidllem  31049  qtophaus  31189  ordtconnlem1  31277  elzrhunit  31330  sgnneg  31908  subfacp1lem6  32545  maxidln1  35482  smprngopr  35490  lsatnem0  36341  atncmp  36608  atncvrN  36611  cdlema2N  37088  lhpmatb  37327  lhpat3  37342  cdleme3  37533  cdleme7  37545  cdlemg27b  37992  dvh2dimatN  38736  dvh2dim  38741  dochexmidlem1  38756  dochfln0  38773
  Copyright terms: Public domain W3C validator