Theorem necon2ai 2962

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

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

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 2934

This theorem is referenced by:  necon2i  2967  intex  5281  iin0  5299  opelopabsb  5478  xpord2indlem  8090  ord1eln01  8424  ord2eln012  8425  1ellim  8426  2ellim  8427  0sdom1dom  9149  inf3lem3  9542  cardmin2  9914  pm54.43  9916  pr2ne  9918  canthp1lem2  10567  renepnf  11184  renemnf  11185  lt0ne0d  11706  nnne0ALT  12206  nn0nepnf  12509  hashnemnf  14297  hashnn0n0nn  14344  geolim  15826  geolim2  15827  georeclim  15828  geoisumr  15834  geoisum1c  15836  ramtcl2  16973  lhop1  25991  logdmn0  26617  logcnlem3  26621  bday1  27820  lrold  27903  mulsval  28115  nbgrssovtx  29444  rusgrnumwwlkl1  30054  strlem1  32336  subfacp1lem1  35377  gonan0  35590  goaln0  35591  rankeq1o  36369  dfttc4lem2  36727  poimirlem9  37964  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem32  37987  pssn0  42682  ensucne0  43974  fouriersw  46677  afvvfveq  47608  fdomne0  49337