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

Theorem necon3bi 2816
 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 150 . 2 𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2797 1 𝜑𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1480   ≠ wne 2790 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 2791 This theorem is referenced by:  r19.2zb  4039  pwne  4801  onnev  5817  alephord  8858  ackbij1lem18  9019  fin23lem26  9107  fin1a2lem6  9187  alephom  9367  gchxpidm  9451  egt2lt3  14878  prmodvdslcmf  15694  symgfix2  17776  chfacfisf  20599  chfacfisfcpmat  20600  alexsubALTlem2  21792  alexsubALTlem4  21794  ptcmplem2  21797  nmoid  22486  cxplogb  24458  axlowdimlem17  25772  frgrncvvdeqlem3  27063  frgrncvvdeq  27072  hasheuni  29970  limsucncmpi  32139  matunitlindflem1  33076  poimirlem32  33112  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  dvasin  33167  lsat0cv  33839  pellexlem5  36916  uzfissfz  39041  xralrple2  39069  infxr  39082  icccncfext  39435  ioodvbdlimc1lem1  39483  volioc  39525  fourierdlem32  39693  fourierdlem49  39709  fourierdlem73  39733  fourierswlem  39784  fouriersw  39785  prsal  39875  sge0pr  39948  voliunsge0lem  40026  carageniuncl  40074  isomenndlem  40081  hoimbl  40182
 Copyright terms: Public domain W3C validator