Theorem necon2ai 2989

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  necon2i  2994  intex  5305  iin0  5324  opelopabsb  5505  xpord2indlem  8131  ord1eln01  8469  ord2eln012  8470  1ellim  8471  2ellim  8472  0sdom1dom  9194  inf3lem3  9587  cardmin2  9973  pm54.43  9975  pr2ne  9977  canthp1lem2  10626  renepnf  11245  renemnf  11246  lt0ne0d  11767  nnne0ALT  12265  nn0nepnf  12576  hashnemnf  14371  hashnn0n0nn  14418  geolim  15914  geolim2  15915  georeclim  15916  geoisumr  15922  geoisum1c  15924  ramtcl2  17061  lhop1  26134  logdmn0  26763  logcnlem3  26767  bday1  27965  lrold  28048  mulsval  28260  nbgrssovtx  29620  rusgrnumwwlkl1  30229  strlem1  32511  subfacp1lem1  35542  gonan0  35755  goaln0  35756  rankeq1o  36534  dfttc4lem2  36902  poimirlem9  38140  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem32  38163  pssn0  42858  ensucne0  44117  fouriersw  46803  afvvfveq  47740  fdomne0  49479