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

Theorem necon3bi 3047
 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 3028 1 𝜑𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1530   ≠ wne 3021 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 3022 This theorem is referenced by:  r19.2zb  4444  pwne  5248  onnev  6310  alephord  9495  ackbij1lem18  9653  fin23lem26  9741  fin1a2lem6  9821  alephom  10001  gchxpidm  10085  egt2lt3  15554  nn0onn  15726  prmodvdslcmf  16378  symgfix2  18480  alexsubALTlem2  22591  alexsubALTlem4  22593  ptcmplem2  22596  nmoid  23285  cxplogb  25296  axlowdimlem17  26677  frgrncvvdeq  28021  hashxpe  30461  hasheuni  31249  limsucncmpi  33696  matunitlindflem1  34774  poimirlem32  34810  ovoliunnfl  34820  voliunnfl  34822  volsupnfl  34823  dvasin  34864  lsat0cv  36055  pellexlem5  39314  uzfissfz  41478  xralrple2  41506  infxr  41519  icccncfext  42054  ioodvbdlimc1lem1  42100  volioc  42141  fourierdlem32  42309  fourierdlem49  42325  fourierdlem73  42349  fourierswlem  42400  fouriersw  42401  sge0pr  42561  voliunsge0lem  42639  carageniuncl  42690  isomenndlem  42697  hoimbl  42798
 Copyright terms: Public domain W3C validator