Theorem necon2ai 2954

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

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

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 2926

This theorem is referenced by:  necon2i  2959  intex  5286  iin0  5304  opelopabsb  5477  xpord2indlem  8087  ord1eln01  8421  ord2eln012  8422  1ellim  8423  2ellim  8424  0sdom1dom  9145  inf3lem3  9545  cardmin2  9914  pm54.43  9916  pr2ne  9918  canthp1lem2  10566  renepnf  11182  renemnf  11183  lt0ne0d  11703  nnne0ALT  12184  nn0nepnf  12483  hashnemnf  14269  hashnn0n0nn  14316  geolim  15795  geolim2  15796  georeclim  15797  geoisumr  15803  geoisum1c  15805  ramtcl2  16941  lhop1  25935  logdmn0  26565  logcnlem3  26569  bday1s  27763  lrold  27829  mulsval  28035  nbgrssovtx  29324  rusgrnumwwlkl1  29931  strlem1  32212  subfacp1lem1  35151  gonan0  35364  goaln0  35365  rankeq1o  36144  poimirlem9  37608  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem32  37631  pssn0  42200  ensucne0  43502  fouriersw  46213  afvvfveq  47133  fdomne0  48835