Theorem necon3bi 2965

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  r19.2zb  4502  pwne  5359  alephord  10113  ackbij1lem18  10274  fin23lem26  10363  fin1a2lem6  10443  alephom  10623  gchxpidm  10707  egt2lt3  16239  nn0onn  16414  prmodvdslcmf  17081  symgfix2  19449  alexsubALTlem2  24072  alexsubALTlem4  24074  ptcmplem2  24077  nmoid  24779  cxplogb  26844  axlowdimlem17  28988  frgrncvvdeq  30338  hashxpe  32817  hasheuni  34066  limsucncmpi  36428  matunitlindflem1  37603  poimirlem32  37639  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  dvasin  37691  lsat0cv  39015  unitscyglem4  42180  metakunt24  42210  readvrec2  42370  readvrec  42371  pellexlem5  42821  uzfissfz  45276  xralrple2  45304  infxr  45317  icccncfext  45843  ioodvbdlimc1lem1  45887  volioc  45928  fourierdlem32  46095  fourierdlem49  46111  fourierdlem73  46135  fourierswlem  46186  fouriersw  46187  sge0pr  46350  voliunsge0lem  46428  carageniuncl  46479  isomenndlem  46486  hoimbl  46587