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

Theorem necon2ai 2695
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 120 . 2  |-  ( ph  ->  -.  A  =  B )
32neqned 2663 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1374    =/= wne 2655
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 185  df-ne 2657
This theorem is referenced by:  necon2i  2703  neneqadOLD  2769  intex  4596  iin0  4614  opelopabsb  4750  0ellim  4933  inf3lem3  8036  cardmin2  8368  pm54.43  8370  canthp1lem2  9020  renepnf  9630  renemnf  9631  lt0ne0d  10107  nnne0  10557  hashnemnf  12372  hashnn0n0nn  12413  geolim  13631  geolim2  13632  georeclim  13633  geoisumr  13639  geoisum1c  13641  ramtcl2  14377  lhop1  22143  logdmn0  22742  logcnlem3  22746  rusgranumwlkl1  24609  vcoprne  25134  strlem1  26831  subfacp1lem1  28249  rankeq1o  29391  afvvfveq  31655
  Copyright terms: Public domain W3C validator