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

Theorem necon3bi 2966
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 154 . 2 𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2946 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2939
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 207  df-ne 2940
This theorem is referenced by:  r19.2zb  4495  pwne  5352  alephord  10116  ackbij1lem18  10277  fin23lem26  10366  fin1a2lem6  10446  alephom  10626  gchxpidm  10710  egt2lt3  16243  nn0onn  16418  prmodvdslcmf  17086  symgfix2  19435  alexsubALTlem2  24057  alexsubALTlem4  24059  ptcmplem2  24062  nmoid  24764  cxplogb  26830  axlowdimlem17  28974  frgrncvvdeq  30329  hashxpe  32812  hasheuni  34087  limsucncmpi  36447  matunitlindflem1  37624  poimirlem32  37660  ovoliunnfl  37670  voliunnfl  37672  volsupnfl  37673  dvasin  37712  lsat0cv  39035  unitscyglem4  42200  metakunt24  42230  readvrec2  42396  readvrec  42397  pellexlem5  42849  uzfissfz  45342  xralrple2  45370  infxr  45383  icccncfext  45907  ioodvbdlimc1lem1  45951  volioc  45992  fourierdlem32  46159  fourierdlem49  46175  fourierdlem73  46199  fourierswlem  46250  fouriersw  46251  sge0pr  46414  voliunsge0lem  46492  carageniuncl  46543  isomenndlem  46550  hoimbl  46651
  Copyright terms: Public domain W3C validator