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

Theorem necon3bbid 2978
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 2977 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 222 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:  necon1abid  2979  necon3bid  2985  eldifsn  4751  php  9160  phpOLD  9172  xmullem2  13193  seqcoll2  14373  cnpart  15134  rlimrecl  15471  ncoprmgcdne1b  16534  prmrp  16596  4sqlem17  16841  mrieqvd  17526  mrieqv2d  17527  pltval  18229  latnlemlt  18369  latnle  18370  odnncl  19335  gexnnod  19378  sylow1lem1  19388  slwpss  19402  lssnle  19464  nzrunit  20205  lspsnne1  20623  cnsubrg  20880  psrridm  21396  mhpmulcl  21562  cmpfi  22782  hausdiag  23019  txhaus  23021  isusp  23636  recld2  24200  metdseq0  24240  i1f1lem  25076  aaliou2b  25724  dvloglem  26026  logf1o2  26028  lgsne0  26706  lgsqr  26722  2sqlem7  26795  ostth3  27009  tglngne  27541  tgelrnln  27621  eucrct2eupth  29238  norm1exi  30241  atnemeq0  31368  opeldifid  31570  pridln1  32270  mxidln1  32290  ssmxidllem  32293  qtophaus  32481  ordtconnlem1  32569  elzrhunit  32624  sgnneg  33204  subfacp1lem6  33843  maxidln1  36553  smprngopr  36561  lsatnem0  37557  atncmp  37824  atncvrN  37827  cdlema2N  38305  lhpmatb  38544  lhpat3  38559  cdleme3  38750  cdleme7  38762  cdlemg27b  39209  dvh2dimatN  39953  dvh2dim  39958  dochexmidlem1  39973  dochfln0  39990  dvrelog2b  40573  aks6d1c2p2  40599  imadrhmcl  40765  nna4b4nsq  41045
  Copyright terms: Public domain W3C validator