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

Theorem necon3bbid 2980
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 222 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 2979 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 222 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1542  wne 2942
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 2943
This theorem is referenced by:  necon1abid  2981  necon3bid  2987  eldifsn  4746  php  9113  phpOLD  9125  xmullem2  13139  seqcoll2  14318  cnpart  15085  rlimrecl  15422  ncoprmgcdne1b  16486  prmrp  16548  4sqlem17  16793  mrieqvd  17478  mrieqv2d  17479  pltval  18181  latnlemlt  18321  latnle  18322  odnncl  19286  gexnnod  19329  sylow1lem1  19339  slwpss  19353  lssnle  19415  lspsnne1  20531  nzrunit  20690  cnsubrg  20810  psrridm  21325  mhpmulcl  21491  cmpfi  22711  hausdiag  22948  txhaus  22950  isusp  23565  recld2  24129  metdseq0  24169  i1f1lem  25005  aaliou2b  25653  dvloglem  25955  logf1o2  25957  lgsne0  26635  lgsqr  26651  2sqlem7  26724  ostth3  26938  tglngne  27321  tgelrnln  27401  eucrct2eupth  29018  norm1exi  30021  atnemeq0  31148  opeldifid  31345  pridln1  32035  mxidln1  32055  ssmxidllem  32058  qtophaus  32221  ordtconnlem1  32309  elzrhunit  32364  sgnneg  32944  subfacp1lem6  33583  maxidln1  36435  smprngopr  36443  lsatnem0  37439  atncmp  37706  atncvrN  37709  cdlema2N  38187  lhpmatb  38426  lhpat3  38441  cdleme3  38632  cdleme7  38644  cdlemg27b  39091  dvh2dimatN  39835  dvh2dim  39840  dochexmidlem1  39855  dochfln0  39872  dvrelog2b  40455  aks6d1c2p2  40481  nna4b4nsq  40901
  Copyright terms: Public domain W3C validator