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

Theorem necon3bi 2804
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 148 . 2 𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2785 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2776
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 195  df-ne 2778
This theorem is referenced by:  r19.2zb  4009  pwne  4749  onnev  5748  alephord  8755  ackbij1lem18  8916  fin23lem26  9004  fin1a2lem6  9084  alephom  9260  gchxpidm  9344  egt2lt3  14716  prmodvdslcmf  15532  symgfix2  17602  chfacfisf  20417  chfacfisfcpmat  20418  alexsubALTlem2  21601  alexsubALTlem4  21603  ptcmplem2  21606  nmoid  22285  cxplogb  24238  axlowdimlem17  25553  2trllemA  25843  2pthon  25895  2pthon3v  25897  frgrancvvdeqlem3  26322  frgrancvvdeqlem9  26331  hasheuni  29277  limsucncmpi  31417  matunitlindflem1  32375  poimirlem32  32411  ovoliunnfl  32421  voliunnfl  32423  volsupnfl  32424  dvasin  32466  lsat0cv  33138  pellexlem5  36215  uzfissfz  38284  xralrple2  38312  infxr  38325  icccncfext  38574  ioodvbdlimc1lem1  38622  volioc  38665  fourierdlem32  38833  fourierdlem49  38849  fourierdlem73  38873  fourierswlem  38924  fouriersw  38925  prsal  39015  sge0pr  39088  voliunsge0lem  39166  carageniuncl  39214  isomenndlem  39221  hoimbl  39322  frgrncvvdeqlem3  41470  frgrncvvdeq  41479
  Copyright terms: Public domain W3C validator