Theorem necon3bi 2973

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

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

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 2947

This theorem is referenced by:  r19.2zb  4519  pwne  5371  alephord  10144  ackbij1lem18  10305  fin23lem26  10394  fin1a2lem6  10474  alephom  10654  gchxpidm  10738  egt2lt3  16254  nn0onn  16428  prmodvdslcmf  17094  symgfix2  19458  alexsubALTlem2  24077  alexsubALTlem4  24079  ptcmplem2  24082  nmoid  24784  cxplogb  26847  axlowdimlem17  28991  frgrncvvdeq  30341  hashxpe  32814  hasheuni  34049  limsucncmpi  36411  matunitlindflem1  37576  poimirlem32  37612  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  dvasin  37664  lsat0cv  38989  unitscyglem4  42155  metakunt24  42185  pellexlem5  42789  uzfissfz  45241  xralrple2  45269  infxr  45282  icccncfext  45808  ioodvbdlimc1lem1  45852  volioc  45893  fourierdlem32  46060  fourierdlem49  46076  fourierdlem73  46100  fourierswlem  46151  fouriersw  46152  sge0pr  46315  voliunsge0lem  46393  carageniuncl  46444  isomenndlem  46451  hoimbl  46552