Theorem necon2ai 2823

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon2i  2828  intex  4820  iin0  4839  opelopabsb  4985  0ellim  5787  inf3lem3  8527  cardmin2  8824  pm54.43  8826  canthp1lem2  9475  renepnf  10087  renemnf  10088  lt0ne0d  10593  nnne0  11053  nn0nepnf  11371  hashnemnf  13132  hashnn0n0nn  13180  geolim  14601  geolim2  14602  georeclim  14603  geoisumr  14609  geoisum1c  14611  ramtcl2  15715  lhop1  23777  logdmn0  24386  logcnlem3  24390  rusgrnumwwlkl1  26863  strlem1  29109  subfacp1lem1  31161  rankeq1o  32278  poimirlem9  33418  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem32  33441  fouriersw  40448  afvvfveq  41228