Theorem necon2ai 2811

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon2i  2816  intex  4747  iin0  4765  opelopabsb  4910  0ellim  5704  inf3lem3  8410  cardmin2  8707  pm54.43  8709  canthp1lem2  9354  renepnf  9966  renemnf  9967  lt0ne0d  10472  nnne0  10930  nn0nepnf  11248  hashnemnf  12994  hashnn0n0nn  13041  geolim  14440  geolim2  14441  georeclim  14442  geoisumr  14448  geoisum1c  14450  ramtcl2  15553  lhop1  23581  logdmn0  24186  logcnlem3  24190  rusgranumwlkl1  26474  strlem1  28493  subfacp1lem1  30415  rankeq1o  31448  poimirlem9  32588  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem32  32611  fouriersw  39124  afvvfveq  39877  rusgrnumwwlkl1  41172