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

Theorem necon2ai 2660
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  |-  ( A  =  B  ->  -.  ph )
Assertion
Ref Expression
necon2ai  |-  ( ph  ->  A  =/=  B )

Proof of Theorem necon2ai
StepHypRef Expression
1 necon2ai.1 . . 3  |-  ( A  =  B  ->  -.  ph )
21con2i 124 . 2  |-  ( ph  ->  -.  A  =  B )
32neqned 2628 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1438    =/= wne 2619
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 189  df-ne 2621
This theorem is referenced by:  necon2i  2668  neneqadOLD  2734  intex  4578  iin0  4596  opelopabsb  4728  0ellim  5502  inf3lem3  8139  cardmin2  8435  pm54.43  8437  canthp1lem2  9080  renepnf  9690  renemnf  9691  lt0ne0d  10181  nnne0  10644  hashnemnf  12528  hashnn0n0nn  12571  geolim  13919  geolim2  13920  georeclim  13921  geoisumr  13927  geoisum1c  13929  ramtcl2  14959  ramtcl2OLD  14960  lhop1  22958  logdmn0  23577  logcnlem3  23581  rusgranumwlkl1  25667  vcoprne  26190  strlem1  27895  subfacp1lem1  29904  rankeq1o  30937  poimirlem9  31907  poimirlem18  31916  poimirlem19  31917  poimirlem20  31918  poimirlem32  31930  fouriersw  37959  afvvfveq  38406
  Copyright terms: Public domain W3C validator