Theorem necon2ai 2969

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

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

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 2940

This theorem is referenced by:  necon2i  2974  intex  5337  iin0  5360  opelopabsb  5530  0ellim  6427  xpord2indlem  8137  ord1eln01  8500  ord2eln012  8501  1ellim  8502  2ellim  8503  0sdom1dom  9242  inf3lem3  9629  cardmin2  9998  pm54.43  10000  pr2ne  10003  canthp1lem2  10652  renepnf  11267  renemnf  11268  lt0ne0d  11784  nnne0ALT  12255  nn0nepnf  12557  hashnemnf  14309  hashnn0n0nn  14356  geolim  15821  geolim2  15822  georeclim  15823  geoisumr  15829  geoisum1c  15831  ramtcl2  16949  lhop1  25767  logdmn0  26385  logcnlem3  26389  bday1s  27570  lrold  27629  mulsval  27805  nbgrssovtx  28886  rusgrnumwwlkl1  29490  strlem1  31771  subfacp1lem1  34469  gonan0  34682  goaln0  34683  rankeq1o  35448  poimirlem9  36801  poimirlem18  36810  poimirlem19  36811  poimirlem20  36812  poimirlem32  36824  pssn0  41352  ensucne0  42583  fouriersw  45246  afvvfveq  46155  fdomne0  47604