Theorem necon3bi 2970

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 2944

This theorem is referenced by:  r19.2zb  4426  pwne  5273  onnevOLD  6388  alephord  9831  ackbij1lem18  9993  fin23lem26  10081  fin1a2lem6  10161  alephom  10341  gchxpidm  10425  egt2lt3  15915  nn0onn  16089  prmodvdslcmf  16748  symgfix2  19024  alexsubALTlem2  23199  alexsubALTlem4  23201  ptcmplem2  23204  nmoid  23906  cxplogb  25936  axlowdimlem17  27326  frgrncvvdeq  28673  hashxpe  31127  hasheuni  32053  limsucncmpi  34634  matunitlindflem1  35773  poimirlem32  35809  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  dvasin  35861  lsat0cv  37047  metakunt24  40148  pellexlem5  40655  uzfissfz  42865  xralrple2  42893  infxr  42906  icccncfext  43428  ioodvbdlimc1lem1  43472  volioc  43513  fourierdlem32  43680  fourierdlem49  43696  fourierdlem73  43720  fourierswlem  43771  fouriersw  43772  sge0pr  43932  voliunsge0lem  44010  carageniuncl  44061  isomenndlem  44068  hoimbl  44169