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  4459  pwne  5308  alephord  10028  ackbij1lem18  10189  fin23lem26  10278  fin1a2lem6  10358  alephom  10538  gchxpidm  10622  egt2lt3  16174  nn0onn  16350  prmodvdslcmf  17018  symgfix2  19346  alexsubALTlem2  23935  alexsubALTlem4  23937  ptcmplem2  23940  nmoid  24630  cxplogb  26696  axlowdimlem17  28885  frgrncvvdeq  30238  hashxpe  32732  hasheuni  34075  limsucncmpi  36433  matunitlindflem1  37610  poimirlem32  37646  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  dvasin  37698  lsat0cv  39026  unitscyglem4  42186  readvrec2  42349  readvrec  42350  pellexlem5  42821  uzfissfz  45322  xralrple2  45350  infxr  45363  icccncfext  45885  ioodvbdlimc1lem1  45929  volioc  45970  fourierdlem32  46137  fourierdlem49  46153  fourierdlem73  46177  fourierswlem  46228  fouriersw  46229  sge0pr  46392  voliunsge0lem  46470  carageniuncl  46521  isomenndlem  46528  hoimbl  46629