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

Theorem necon2ai 2672
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 2650 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1452    =/= wne 2641
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 190  df-ne 2643
This theorem is referenced by:  necon2i  2677  intex  4557  iin0  4575  opelopabsb  4711  0ellim  5492  inf3lem3  8153  cardmin2  8450  pm54.43  8452  canthp1lem2  9096  renepnf  9706  renemnf  9707  lt0ne0d  10200  nnne0  10664  hashnemnf  12565  hashnn0n0nn  12608  geolim  14003  geolim2  14004  georeclim  14005  geoisumr  14011  geoisum1c  14013  ramtcl2  15045  ramtcl2OLD  15046  lhop1  23045  logdmn0  23664  logcnlem3  23668  rusgranumwlkl1  25754  vcoprne  26279  strlem1  27984  subfacp1lem1  29974  rankeq1o  31009  poimirlem9  32013  poimirlem18  32022  poimirlem19  32023  poimirlem20  32024  poimirlem32  32036  fouriersw  38207  afvvfveq  38795  nn0nepnf  39229
  Copyright terms: Public domain W3C validator