Theorem necon2ai 2964

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon2i  2969  intex  5279  iin0  5298  opelopabsb  5479  xpord2indlem  8094  ord1eln01  8428  ord2eln012  8429  1ellim  8430  2ellim  8431  0sdom1dom  9153  inf3lem3  9549  cardmin2  9921  pm54.43  9923  pr2ne  9925  canthp1lem2  10574  renepnf  11191  renemnf  11192  lt0ne0d  11713  nnne0ALT  12213  nn0nepnf  12516  hashnemnf  14304  hashnn0n0nn  14351  geolim  15833  geolim2  15834  georeclim  15835  geoisumr  15841  geoisum1c  15843  ramtcl2  16980  lhop1  26006  logdmn0  26629  logcnlem3  26633  bday1  27831  lrold  27914  mulsval  28126  nbgrssovtx  29455  rusgrnumwwlkl1  30064  strlem1  32346  subfacp1lem1  35414  gonan0  35627  goaln0  35628  rankeq1o  36406  dfttc4lem2  36764  poimirlem9  38003  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem32  38026  pssn0  42721  ensucne0  43980  fouriersw  46681  afvvfveq  47618  fdomne0  49347