Theorem necon2ai 3047

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 3019

This theorem is referenced by:  necon2i  3052  intex  5242  iin0  5263  opelopabsb  5419  0ellim  6255  inf3lem3  9095  cardmin2  9429  pm54.43  9431  canthp1lem2  10077  renepnf  10691  renemnf  10692  lt0ne0d  11207  nnne0ALT  11678  nn0nepnf  11978  hashnemnf  13707  hashnn0n0nn  13755  geolim  15228  geolim2  15229  georeclim  15230  geoisumr  15236  geoisum1c  15238  ramtcl2  16349  lhop1  24613  logdmn0  25225  logcnlem3  25229  nbgrssovtx  27145  rusgrnumwwlkl1  27749  strlem1  30029  subfacp1lem1  32428  gonan0  32641  goaln0  32642  rankeq1o  33634  poimirlem9  34903  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem32  34926  pssn0  39120  ensucne0  39902  fouriersw  42523  afvvfveq  43354