Theorem necon2ai 2984

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon2i  2989  intex  5304  iin0  5323  opelopabsb  5503  xpord2indlem  8166  ord1eln01  8507  ord2eln012  8508  1ellim  8509  2ellim  8510  0sdom1dom  9240  inf3lem3  9634  cardmin2  10083  pm54.43  10085  pr2ne  10087  canthp1lem2  10741  renepnf  11360  renemnf  11361  lt0ne0d  11884  nnne0ALT  12379  nn0nepnf  12690  hashnemnf  14491  hashnn0n0nn  14538  geolim  16044  geolim2  16045  georeclim  16046  geoisumr  16052  geoisum1c  16054  ramtcl2  17194  lhop1  26339  logdmn0  26973  logcnlem3  26977  bday1  28205  lrold  28288  mulsval  28500  nbgrssovtx  29947  rusgrnumwwlkl1  30565  strlem1  32857  subfacp1lem1  36030  gonan0  36243  goaln0  36244  rankeq1o  37024  dfttc4lem2  37409  poimirlem9  38640  poimirlem18  38649  poimirlem19  38650  poimirlem20  38651  poimirlem32  38663  pssn0  43374  ensucne0  44623  fouriersw  47334  afvvfveq  48311  fdomne0  50054