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

Theorem necon3bbid 2860
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 213 . . 3 (𝜑 → (𝐴 = 𝐵𝜓))
32necon3abid 2859 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
43bicomd 213 1 (𝜑 → (¬ 𝜓𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon1abid  2861  necon3bid  2867  eldifsn  4350  php  8185  xmullem2  12133  seqcoll2  13287  cnpart  14024  rlimrecl  14355  ncoprmgcdne1b  15410  prmrp  15471  4sqlem17  15712  mrieqvd  16345  mrieqv2d  16346  pltval  17007  latnlemlt  17131  latnle  17132  odnncl  18010  gexnnod  18049  sylow1lem1  18059  slwpss  18073  lssnle  18133  lspsnne1  19165  nzrunit  19315  psrridm  19452  cnsubrg  19854  cmpfi  21259  hausdiag  21496  txhaus  21498  isusp  22112  recld2  22664  metdseq0  22704  i1f1lem  23501  aaliou2b  24141  dvloglem  24439  logf1o2  24441  lgsne0  25105  lgsqr  25121  2sqlem7  25194  ostth3  25372  tglngne  25490  tgelrnln  25570  eucrct2eupth  27223  norm1exi  28235  atnemeq0  29364  opeldifid  29538  qtophaus  30031  ordtconnlem1  30098  elzrhunit  30151  sgnneg  30730  subfacp1lem6  31293  maxidln1  33973  smprngopr  33981  lsatnem0  34650  atncmp  34917  atncvrN  34920  cdlema2N  35396  lhpmatb  35635  lhpat3  35650  cdleme3  35842  cdleme7  35854  cdlemg27b  36301  dvh2dimatN  37046  dvh2dim  37051  dochexmidlem1  37066  dochfln0  37083
  Copyright terms: Public domain W3C validator