Theorem necon2ai 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  necon2i  2960  intex  5302  iin0  5320  opelopabsb  5493  xpord2indlem  8129  ord1eln01  8463  ord2eln012  8464  1ellim  8465  2ellim  8466  0sdom1dom  9192  inf3lem3  9590  cardmin2  9959  pm54.43  9961  pr2ne  9964  canthp1lem2  10613  renepnf  11229  renemnf  11230  lt0ne0d  11750  nnne0ALT  12231  nn0nepnf  12530  hashnemnf  14316  hashnn0n0nn  14363  geolim  15843  geolim2  15844  georeclim  15845  geoisumr  15851  geoisum1c  15853  ramtcl2  16989  lhop1  25926  logdmn0  26556  logcnlem3  26560  bday1s  27750  lrold  27815  mulsval  28019  nbgrssovtx  29295  rusgrnumwwlkl1  29905  strlem1  32186  subfacp1lem1  35173  gonan0  35386  goaln0  35387  rankeq1o  36166  poimirlem9  37630  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem32  37653  pssn0  42222  ensucne0  43525  fouriersw  46236  afvvfveq  47153  fdomne0  48842