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

Theorem necon2ai 2852
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 134 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
32neqned 2830 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon2i  2857  intex  4850  iin0  4869  opelopabsb  5014  0ellim  5825  inf3lem3  8565  cardmin2  8862  pm54.43  8864  canthp1lem2  9513  renepnf  10125  renemnf  10126  lt0ne0d  10631  nnne0  11091  nn0nepnf  11409  hashnemnf  13172  hashnn0n0nn  13218  geolim  14645  geolim2  14646  georeclim  14647  geoisumr  14653  geoisum1c  14655  ramtcl2  15762  lhop1  23822  logdmn0  24431  logcnlem3  24435  nbgrssovtx  26302  rusgrnumwwlkl1  26935  strlem1  29237  subfacp1lem1  31287  rankeq1o  32403  poimirlem9  33548  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem32  33571  fouriersw  40766  afvvfveq  41549
  Copyright terms: Public domain W3C validator