Theorem necon3bi 2808

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 149	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2789	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  r19.2zb  4013  pwne  4757  onnev  5765  alephord  8781  ackbij1lem18  8942  fin23lem26  9030  fin1a2lem6  9110  alephom  9286  gchxpidm  9370  egt2lt3  14773  prmodvdslcmf  15589  symgfix2  17659  chfacfisf  20478  chfacfisfcpmat  20479  alexsubALTlem2  21662  alexsubALTlem4  21664  ptcmplem2  21667  nmoid  22356  cxplogb  24324  axlowdimlem17  25638  2trllemA  26080  2pthon  26132  2pthon3v  26134  frgrancvvdeqlem3  26559  frgrancvvdeqlem9  26568  hasheuni  29474  limsucncmpi  31614  matunitlindflem1  32575  poimirlem32  32611  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  dvasin  32666  lsat0cv  33338  pellexlem5  36415  uzfissfz  38483  xralrple2  38511  infxr  38524  icccncfext  38773  ioodvbdlimc1lem1  38821  volioc  38864  fourierdlem32  39032  fourierdlem49  39048  fourierdlem73  39072  fourierswlem  39123  fouriersw  39124  prsal  39214  sge0pr  39287  voliunsge0lem  39365  carageniuncl  39413  isomenndlem  39420  hoimbl  39521  frgrncvvdeqlem3  41471  frgrncvvdeq  41480