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

Theorem necon3bi 2849
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 2830 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  r19.2zb  4094  pwne  4861  onnev  5886  alephord  8936  ackbij1lem18  9097  fin23lem26  9185  fin1a2lem6  9265  alephom  9445  gchxpidm  9529  egt2lt3  14978  prmodvdslcmf  15798  symgfix2  17882  chfacfisf  20707  chfacfisfcpmat  20708  alexsubALTlem2  21899  alexsubALTlem4  21901  ptcmplem2  21904  nmoid  22593  cxplogb  24569  axlowdimlem17  25883  frgrncvvdeq  27289  hasheuni  30275  limsucncmpi  32569  matunitlindflem1  33535  poimirlem32  33571  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  dvasin  33626  lsat0cv  34638  pellexlem5  37714  uzfissfz  39855  xralrple2  39883  infxr  39896  icccncfext  40418  ioodvbdlimc1lem1  40464  volioc  40506  fourierdlem32  40674  fourierdlem49  40690  fourierdlem73  40714  fourierswlem  40765  fouriersw  40766  prsal  40856  sge0pr  40929  voliunsge0lem  41007  carageniuncl  41058  isomenndlem  41065  hoimbl  41166
  Copyright terms: Public domain W3C validator