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

Theorem necon3bi 2960
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon3bi.1 (𝐴 = 𝐵𝜑)
Assertion
Ref Expression
necon3bi 𝜑𝐴𝐵)

Proof of Theorem necon3bi
StepHypRef Expression
1 necon3bi.1 . . 3 (𝐴 = 𝐵𝜑)
21con3i 157 . 2 𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2941 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2934
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 2935
This theorem is referenced by:  r19.2zb  4382  pwne  5217  onnevOLD  6294  alephord  9575  ackbij1lem18  9737  fin23lem26  9825  fin1a2lem6  9905  alephom  10085  gchxpidm  10169  egt2lt3  15651  nn0onn  15825  prmodvdslcmf  16483  symgfix2  18662  alexsubALTlem2  22799  alexsubALTlem4  22801  ptcmplem2  22804  nmoid  23495  cxplogb  25524  axlowdimlem17  26904  frgrncvvdeq  28246  hashxpe  30702  hasheuni  31623  limsucncmpi  34272  matunitlindflem1  35396  poimirlem32  35432  ovoliunnfl  35442  voliunnfl  35444  volsupnfl  35445  dvasin  35484  lsat0cv  36670  metakunt24  39739  pellexlem5  40227  uzfissfz  42403  xralrple2  42431  infxr  42444  icccncfext  42970  ioodvbdlimc1lem1  43014  volioc  43055  fourierdlem32  43222  fourierdlem49  43238  fourierdlem73  43262  fourierswlem  43313  fouriersw  43314  sge0pr  43474  voliunsge0lem  43552  carageniuncl  43603  isomenndlem  43610  hoimbl  43711
  Copyright terms: Public domain W3C validator