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 1540   ≠ 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  5314  iin0  5332  opelopabsb  5505  0ellim  6416  xpord2indlem  8146  ord1eln01  8508  ord2eln012  8509  1ellim  8510  2ellim  8511  0sdom1dom  9246  inf3lem3  9644  cardmin2  10013  pm54.43  10015  pr2ne  10018  canthp1lem2  10667  renepnf  11283  renemnf  11284  lt0ne0d  11802  nnne0ALT  12278  nn0nepnf  12582  hashnemnf  14362  hashnn0n0nn  14409  geolim  15886  geolim2  15887  georeclim  15888  geoisumr  15894  geoisum1c  15896  ramtcl2  17031  lhop1  25971  logdmn0  26601  logcnlem3  26605  bday1s  27795  lrold  27860  mulsval  28064  nbgrssovtx  29340  rusgrnumwwlkl1  29950  strlem1  32231  subfacp1lem1  35201  gonan0  35414  goaln0  35415  rankeq1o  36189  poimirlem9  37653  poimirlem18  37662  poimirlem19  37663  poimirlem20  37664  poimirlem32  37676  pssn0  42278  ensucne0  43553  fouriersw  46260  afvvfveq  47177  fdomne0  48828