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

Theorem necon2ai 2807
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 132 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2785 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2776
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 195  df-ne 2778
This theorem is referenced by:  necon2i  2812  intex  4739  iin0  4757  opelopabsb  4897  0ellim  5687  inf3lem3  8384  cardmin2  8681  pm54.43  8683  canthp1lem2  9328  renepnf  9940  renemnf  9941  lt0ne0d  10439  nnne0  10897  hashnemnf  12943  hashnn0n0nn  12990  geolim  14383  geolim2  14384  georeclim  14385  geoisumr  14391  geoisum1c  14393  ramtcl2  15496  lhop1  23495  logdmn0  24100  logcnlem3  24104  rusgranumwlkl1  26237  vcoprneOLD  26597  strlem1  28296  subfacp1lem1  30218  rankeq1o  31251  poimirlem9  32388  poimirlem18  32397  poimirlem19  32398  poimirlem20  32399  poimirlem32  32411  fouriersw  38925  afvvfveq  39679  nn0nepnf  40205  rusgrnumwwlkl1  41171
  Copyright terms: Public domain W3C validator