Theorem necon2ai 3000

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 137	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2978	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1653   ≠ wne 2971

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 199  df-ne 2972

This theorem is referenced by:  necon2i  3005  intex  5012  iin0  5031  opelopabsb  5181  0ellim  6003  inf3lem3  8777  cardmin2  9110  pm54.43  9112  canthp1lem2  9763  renepnf  10376  renemnf  10377  lt0ne0d  10885  nnne0ALT  11351  nn0nepnf  11660  hashnemnf  13384  hashnn0n0nn  13430  geolim  14939  geolim2  14940  georeclim  14941  geoisumr  14947  geoisum1c  14949  ramtcl2  16048  lhop1  24118  logdmn0  24727  logcnlem3  24731  nbgrssovtx  26599  rusgrnumwwlkl1  27259  strlem1  29634  subfacp1lem1  31678  rankeq1o  32791  poimirlem9  33907  poimirlem18  33916  poimirlem19  33917  poimirlem20  33918  poimirlem32  33930  pssn0  38035  fouriersw  41191  afvvfveq  42002