Theorem necon3bi 2966

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 2946	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

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

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 2940

This theorem is referenced by:  r19.2zb  4495  pwne  5350  onnevOLD  6492  alephord  10073  ackbij1lem18  10235  fin23lem26  10323  fin1a2lem6  10403  alephom  10583  gchxpidm  10667  egt2lt3  16154  nn0onn  16328  prmodvdslcmf  16985  symgfix2  19326  alexsubALTlem2  23773  alexsubALTlem4  23775  ptcmplem2  23778  nmoid  24480  cxplogb  26528  axlowdimlem17  28484  frgrncvvdeq  29830  hashxpe  32287  hasheuni  33382  limsucncmpi  35634  matunitlindflem1  36788  poimirlem32  36824  ovoliunnfl  36834  voliunnfl  36836  volsupnfl  36837  dvasin  36876  lsat0cv  38207  metakunt24  41315  pellexlem5  41874  uzfissfz  44335  xralrple2  44363  infxr  44376  icccncfext  44902  ioodvbdlimc1lem1  44946  volioc  44987  fourierdlem32  45154  fourierdlem49  45170  fourierdlem73  45194  fourierswlem  45245  fouriersw  45246  sge0pr  45409  voliunsge0lem  45487  carageniuncl  45538  isomenndlem  45545  hoimbl  45646