Theorem necon2ai 2985

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon2i  2990  intex  5299  iin0  5318  opelopabsb  5499  xpord2indlem  8122  ord1eln01  8460  ord2eln012  8461  1ellim  8462  2ellim  8463  0sdom1dom  9186  inf3lem3  9582  cardmin2  9954  pm54.43  9956  pr2ne  9958  canthp1lem2  10608  renepnf  11227  renemnf  11228  lt0ne0d  11749  nnne0ALT  12248  nn0nepnf  12559  hashnemnf  14354  hashnn0n0nn  14401  geolim  15883  geolim2  15884  georeclim  15885  geoisumr  15891  geoisum1c  15893  ramtcl2  17030  lhop1  26056  logdmn0  26682  logcnlem3  26686  bday1  27884  lrold  27967  mulsval  28179  nbgrssovtx  29508  rusgrnumwwlkl1  30117  strlem1  32399  subfacp1lem1  35493  gonan0  35706  goaln0  35707  rankeq1o  36485  dfttc4lem2  36853  poimirlem9  38092  poimirlem18  38101  poimirlem19  38102  poimirlem20  38103  poimirlem32  38115  pssn0  42810  ensucne0  44069  fouriersw  46769  afvvfveq  47706  fdomne0  49435