Theorem necon2ai 2970

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

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

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 2941

This theorem is referenced by:  necon2i  2975  intex  5344  iin0  5362  opelopabsb  5535  0ellim  6447  xpord2indlem  8172  ord1eln01  8534  ord2eln012  8535  1ellim  8536  2ellim  8537  0sdom1dom  9274  inf3lem3  9670  cardmin2  10039  pm54.43  10041  pr2ne  10044  canthp1lem2  10693  renepnf  11309  renemnf  11310  lt0ne0d  11828  nnne0ALT  12304  nn0nepnf  12607  hashnemnf  14383  hashnn0n0nn  14430  geolim  15906  geolim2  15907  georeclim  15908  geoisumr  15914  geoisum1c  15916  ramtcl2  17049  lhop1  26053  logdmn0  26682  logcnlem3  26686  bday1s  27876  lrold  27935  mulsval  28135  nbgrssovtx  29378  rusgrnumwwlkl1  29988  strlem1  32269  subfacp1lem1  35184  gonan0  35397  goaln0  35398  rankeq1o  36172  poimirlem9  37636  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem32  37659  pssn0  42266  ensucne0  43542  fouriersw  46246  afvvfveq  47160  fdomne0  48759