Theorem necon2ai 2961

Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon2ai.1	⊢ (𝐴 = 𝐵 → ¬ 𝜑)

Assertion

Ref	Expression
necon2ai	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem necon2ai

Step	Hyp	Ref	Expression
1		necon2ai.1	. . 3 ⊢ (𝐴 = 𝐵 → ¬ 𝜑)
2	1	con2i 139	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2939	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  necon2i  2966  intex  5285  iin0  5304  opelopabsb  5485  xpord2indlem  8097  ord1eln01  8431  ord2eln012  8432  1ellim  8433  2ellim  8434  0sdom1dom  9156  inf3lem3  9551  cardmin2  9923  pm54.43  9925  pr2ne  9927  canthp1lem2  10576  renepnf  11193  renemnf  11194  lt0ne0d  11715  nnne0ALT  12215  nn0nepnf  12518  hashnemnf  14306  hashnn0n0nn  14353  geolim  15835  geolim2  15836  georeclim  15837  geoisumr  15843  geoisum1c  15845  ramtcl2  16982  lhop1  25981  logdmn0  26604  logcnlem3  26608  bday1  27806  lrold  27889  mulsval  28101  nbgrssovtx  29430  rusgrnumwwlkl1  30039  strlem1  32321  subfacp1lem1  35361  gonan0  35574  goaln0  35575  rankeq1o  36353  dfttc4lem2  36711  poimirlem9  37950  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem32  37973  pssn0  42668  ensucne0  43956  fouriersw  46659  afvvfveq  47596  fdomne0  49325