Theorem necon2ai 2965

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2935

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 206  df-ne 2936

This theorem is referenced by:  necon2i  2970  intex  5333  iin0  5356  opelopabsb  5526  0ellim  6426  xpord2indlem  8146  ord1eln01  8510  ord2eln012  8511  1ellim  8512  2ellim  8513  0sdom1dom  9256  inf3lem3  9647  cardmin2  10016  pm54.43  10018  pr2ne  10021  canthp1lem2  10670  renepnf  11286  renemnf  11287  lt0ne0d  11803  nnne0ALT  12274  nn0nepnf  12576  hashnemnf  14329  hashnn0n0nn  14376  geolim  15842  geolim2  15843  georeclim  15844  geoisumr  15850  geoisum1c  15852  ramtcl2  16973  lhop1  25940  logdmn0  26567  logcnlem3  26571  bday1s  27757  lrold  27816  mulsval  28002  nbgrssovtx  29167  rusgrnumwwlkl1  29772  strlem1  32053  subfacp1lem1  34779  gonan0  34992  goaln0  34993  rankeq1o  35757  poimirlem9  37091  poimirlem18  37100  poimirlem19  37101  poimirlem20  37102  poimirlem32  37114  pssn0  41687  ensucne0  42931  fouriersw  45591  afvvfveq  46500  fdomne0  47874