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

Theorem necon3bbid 3050
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 224 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 3049 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 224 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207   = wceq 1528  wne 3013
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 3014
This theorem is referenced by:  necon1abid  3051  necon3bid  3057  eldifsn  4711  php  8689  xmullem2  12646  seqcoll2  13811  cnpart  14587  rlimrecl  14925  ncoprmgcdne1b  15982  prmrp  16044  4sqlem17  16285  mrieqvd  16897  mrieqv2d  16898  pltval  17558  latnlemlt  17682  latnle  17683  odnncl  18602  gexnnod  18642  sylow1lem1  18652  slwpss  18666  lssnle  18729  lspsnne1  19818  nzrunit  19968  psrridm  20112  cnsubrg  20533  cmpfi  21944  hausdiag  22181  txhaus  22183  isusp  22797  recld2  23349  metdseq0  23389  i1f1lem  24217  aaliou2b  24857  dvloglem  25158  logf1o2  25160  lgsne0  25838  lgsqr  25854  2sqlem7  25927  ostth3  26141  tglngne  26263  tgelrnln  26343  eucrct2eupth  27951  norm1exi  28954  atnemeq0  30081  opeldifid  30277  qtophaus  30999  ordtconnlem1  31066  elzrhunit  31119  sgnneg  31697  subfacp1lem6  32329  maxidln1  35203  smprngopr  35211  lsatnem0  36061  atncmp  36328  atncvrN  36331  cdlema2N  36808  lhpmatb  37047  lhpat3  37062  cdleme3  37253  cdleme7  37265  cdlemg27b  37712  dvh2dimatN  38456  dvh2dim  38461  dochexmidlem1  38476  dochfln0  38493
  Copyright terms: Public domain W3C validator