Theorem necon2ai 3048

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 3019

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 3020

This theorem is referenced by:  necon2i  3053  intex  5243  iin0  5264  opelopabsb  5420  0ellim  6256  inf3lem3  9096  cardmin2  9430  pm54.43  9432  canthp1lem2  10078  renepnf  10692  renemnf  10693  lt0ne0d  11208  nnne0ALT  11678  nn0nepnf  11978  hashnemnf  13707  hashnn0n0nn  13755  geolim  15229  geolim2  15230  georeclim  15231  geoisumr  15237  geoisum1c  15239  ramtcl2  16350  lhop1  24614  logdmn0  25226  logcnlem3  25230  nbgrssovtx  27146  rusgrnumwwlkl1  27750  strlem1  30030  subfacp1lem1  32430  gonan0  32643  goaln0  32644  rankeq1o  33636  poimirlem9  34905  poimirlem18  34914  poimirlem19  34915  poimirlem20  34916  poimirlem32  34928  pssn0  39119  ensucne0  39901  fouriersw  42523  afvvfveq  43354