Theorem necon2ai 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon2i  2963  intex  5284  iin0  5302  opelopabsb  5473  xpord2indlem  8083  ord1eln01  8417  ord2eln012  8418  1ellim  8419  2ellim  8420  0sdom1dom  9137  inf3lem3  9527  cardmin2  9899  pm54.43  9901  pr2ne  9903  canthp1lem2  10551  renepnf  11167  renemnf  11168  lt0ne0d  11689  nnne0ALT  12170  nn0nepnf  12469  hashnemnf  14253  hashnn0n0nn  14300  geolim  15779  geolim2  15780  georeclim  15781  geoisumr  15787  geoisum1c  15789  ramtcl2  16925  lhop1  25947  logdmn0  26577  logcnlem3  26581  bday1s  27776  lrold  27843  mulsval  28049  nbgrssovtx  29341  rusgrnumwwlkl1  29951  strlem1  32232  subfacp1lem1  35244  gonan0  35457  goaln0  35458  rankeq1o  36236  poimirlem9  37689  poimirlem18  37698  poimirlem19  37699  poimirlem20  37700  poimirlem32  37712  pssn0  42345  ensucne0  43646  fouriersw  46353  afvvfveq  47272  fdomne0  48974