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

Theorem necon2ai 2683
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 )
32neneqad 2652 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2644
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 2646
This theorem is referenced by:  necon2i  2691  neneqadOLD  2757  intex  4548  iin0  4566  opelopabsb  4699  0ellim  4881  inf3lem3  7939  cardmin2  8271  pm54.43  8273  canthp1lem2  8923  renepnf  9534  renemnf  9535  lt0ne0d  10008  nnne0  10457  hashnemnf  12218  hashnn0n0nn  12257  geolim  13434  geolim2  13435  georeclim  13436  geoisumr  13442  geoisum1c  13444  ramtcl2  14176  lhop1  21604  logdmn0  22203  logcnlem3  22207  vcoprne  24094  strlem1  25791  subfacp1lem1  27203  rankeq1o  28345  afvvfveq  30194  rusgranumwlkl1  30699
  Copyright terms: Public domain W3C validator