Theorem necon2ai 2966

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

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

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 2937

This theorem is referenced by:  necon2i  2971  intex  5334  iin0  5357  opelopabsb  5527  0ellim  6427  xpord2indlem  8147  ord1eln01  8511  ord2eln012  8512  1ellim  8513  2ellim  8514  0sdom1dom  9257  inf3lem3  9648  cardmin2  10017  pm54.43  10019  pr2ne  10022  canthp1lem2  10671  renepnf  11287  renemnf  11288  lt0ne0d  11804  nnne0ALT  12275  nn0nepnf  12577  hashnemnf  14330  hashnn0n0nn  14377  geolim  15843  geolim2  15844  georeclim  15845  geoisumr  15851  geoisum1c  15853  ramtcl2  16974  lhop1  25941  logdmn0  26568  logcnlem3  26572  bday1s  27758  lrold  27817  mulsval  28003  nbgrssovtx  29168  rusgrnumwwlkl1  29773  strlem1  32054  subfacp1lem1  34784  gonan0  34997  goaln0  34998  rankeq1o  35762  poimirlem9  37097  poimirlem18  37106  poimirlem19  37107  poimirlem20  37108  poimirlem32  37120  pssn0  41706  ensucne0  42950  fouriersw  45610  afvvfveq  46519  fdomne0  47893