MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2ai Structured version   Visualization version   GIF version

Theorem necon2ai 3000
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
StepHypRef Expression
1 necon2ai.1 . . 3 (𝐴 = 𝐵 → ¬ 𝜑)
21con2i 137 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2978 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1653  wne 2971
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 199  df-ne 2972
This theorem is referenced by:  necon2i  3005  intex  5012  iin0  5031  opelopabsb  5181  0ellim  6003  inf3lem3  8777  cardmin2  9110  pm54.43  9112  canthp1lem2  9763  renepnf  10376  renemnf  10377  lt0ne0d  10885  nnne0ALT  11351  nn0nepnf  11660  hashnemnf  13384  hashnn0n0nn  13430  geolim  14939  geolim2  14940  georeclim  14941  geoisumr  14947  geoisum1c  14949  ramtcl2  16048  lhop1  24118  logdmn0  24727  logcnlem3  24731  nbgrssovtx  26599  rusgrnumwwlkl1  27259  strlem1  29634  subfacp1lem1  31678  rankeq1o  32791  poimirlem9  33907  poimirlem18  33916  poimirlem19  33917  poimirlem20  33918  poimirlem32  33930  pssn0  38035  fouriersw  41191  afvvfveq  42002
  Copyright terms: Public domain W3C validator