Theorem necon2ai 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon2i  2967  intex  5279  iin0  5297  opelopabsb  5476  xpord2indlem  8088  ord1eln01  8422  ord2eln012  8423  1ellim  8424  2ellim  8425  0sdom1dom  9147  inf3lem3  9540  cardmin2  9912  pm54.43  9914  pr2ne  9916  canthp1lem2  10565  renepnf  11182  renemnf  11183  lt0ne0d  11704  nnne0ALT  12204  nn0nepnf  12507  hashnemnf  14295  hashnn0n0nn  14342  geolim  15824  geolim2  15825  georeclim  15826  geoisumr  15832  geoisum1c  15834  ramtcl2  16971  lhop1  25991  logdmn0  26620  logcnlem3  26624  bday1  27825  lrold  27908  mulsval  28120  nbgrssovtx  29449  rusgrnumwwlkl1  30059  strlem1  32341  subfacp1lem1  35382  gonan0  35595  goaln0  35596  rankeq1o  36374  dfttc4lem2  36732  poimirlem9  37961  poimirlem18  37970  poimirlem19  37971  poimirlem20  37972  poimirlem32  37984  pssn0  42679  ensucne0  43971  fouriersw  46674  afvvfveq  47593  fdomne0  49322