Theorem necon3bi 2951

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

Step	Hyp	Ref	Expression
1		necon3bi.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝜑)
2	1	con3i 154	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2932	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  r19.2zb  4449  pwne  5295  alephord  9988  ackbij1lem18  10149  fin23lem26  10238  fin1a2lem6  10318  alephom  10498  gchxpidm  10582  egt2lt3  16133  nn0onn  16309  prmodvdslcmf  16977  symgfix2  19313  alexsubALTlem2  23951  alexsubALTlem4  23953  ptcmplem2  23956  nmoid  24646  cxplogb  26712  axlowdimlem17  28921  frgrncvvdeq  30271  hashxpe  32765  hasheuni  34051  limsucncmpi  36418  matunitlindflem1  37595  poimirlem32  37631  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  dvasin  37683  lsat0cv  39011  unitscyglem4  42171  readvrec2  42334  readvrec  42335  pellexlem5  42806  uzfissfz  45306  xralrple2  45334  infxr  45347  icccncfext  45869  ioodvbdlimc1lem1  45913  volioc  45954  fourierdlem32  46121  fourierdlem49  46137  fourierdlem73  46161  fourierswlem  46212  fouriersw  46213  sge0pr  46376  voliunsge0lem  46454  carageniuncl  46505  isomenndlem  46512  hoimbl  46613