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

Theorem necon3bi 2970
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 2950 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1539  wne 2943
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 206  df-ne 2944
This theorem is referenced by:  r19.2zb  4426  pwne  5273  onnevOLD  6388  alephord  9831  ackbij1lem18  9993  fin23lem26  10081  fin1a2lem6  10161  alephom  10341  gchxpidm  10425  egt2lt3  15915  nn0onn  16089  prmodvdslcmf  16748  symgfix2  19024  alexsubALTlem2  23199  alexsubALTlem4  23201  ptcmplem2  23204  nmoid  23906  cxplogb  25936  axlowdimlem17  27326  frgrncvvdeq  28673  hashxpe  31127  hasheuni  32053  limsucncmpi  34634  matunitlindflem1  35773  poimirlem32  35809  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  dvasin  35861  lsat0cv  37047  metakunt24  40148  pellexlem5  40655  uzfissfz  42865  xralrple2  42893  infxr  42906  icccncfext  43428  ioodvbdlimc1lem1  43472  volioc  43513  fourierdlem32  43680  fourierdlem49  43696  fourierdlem73  43720  fourierswlem  43771  fouriersw  43772  sge0pr  43932  voliunsge0lem  44010  carageniuncl  44061  isomenndlem  44068  hoimbl  44169
  Copyright terms: Public domain W3C validator