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

Theorem necon3bi 2967
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 2947 1 𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2940
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 2941
This theorem is referenced by:  r19.2zb  4457  pwne  5311  onnevOLD  6449  alephord  10019  ackbij1lem18  10181  fin23lem26  10269  fin1a2lem6  10349  alephom  10529  gchxpidm  10613  egt2lt3  16096  nn0onn  16270  prmodvdslcmf  16927  symgfix2  19206  alexsubALTlem2  23422  alexsubALTlem4  23424  ptcmplem2  23427  nmoid  24129  cxplogb  26159  axlowdimlem17  27956  frgrncvvdeq  29302  hashxpe  31765  hasheuni  32748  limsucncmpi  34970  matunitlindflem1  36124  poimirlem32  36160  ovoliunnfl  36170  voliunnfl  36172  volsupnfl  36173  dvasin  36212  lsat0cv  37545  metakunt24  40650  pellexlem5  41203  uzfissfz  43651  xralrple2  43679  infxr  43692  icccncfext  44218  ioodvbdlimc1lem1  44262  volioc  44303  fourierdlem32  44470  fourierdlem49  44486  fourierdlem73  44510  fourierswlem  44561  fouriersw  44562  sge0pr  44725  voliunsge0lem  44803  carageniuncl  44854  isomenndlem  44861  hoimbl  44962
  Copyright terms: Public domain W3C validator