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  5291  iin0  5309  opelopabsb  5486  xpord2indlem  8099  ord1eln01  8433  ord2eln012  8434  1ellim  8435  2ellim  8436  0sdom1dom  9158  inf3lem3  9551  cardmin2  9923  pm54.43  9925  pr2ne  9927  canthp1lem2  10576  renepnf  11192  renemnf  11193  lt0ne0d  11714  nnne0ALT  12195  nn0nepnf  12494  hashnemnf  14279  hashnn0n0nn  14326  geolim  15805  geolim2  15806  georeclim  15807  geoisumr  15813  geoisum1c  15815  ramtcl2  16951  lhop1  25987  logdmn0  26617  logcnlem3  26621  bday1  27822  lrold  27905  mulsval  28117  nbgrssovtx  29446  rusgrnumwwlkl1  30056  strlem1  32337  subfacp1lem1  35392  gonan0  35605  goaln0  35606  rankeq1o  36384  poimirlem9  37874  poimirlem18  37883  poimirlem19  37884  poimirlem20  37885  poimirlem32  37897  pssn0  42593  ensucne0  43879  fouriersw  46583  afvvfveq  47502  fdomne0  49203