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

Theorem necon2ai 2655
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 2633 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1446    =/= wne 2624
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 2626
This theorem is referenced by:  necon2i  2660  intex  4562  iin0  4580  opelopabsb  4714  0ellim  5488  inf3lem3  8140  cardmin2  8437  pm54.43  8439  canthp1lem2  9083  renepnf  9693  renemnf  9694  lt0ne0d  10186  nnne0  10649  hashnemnf  12534  hashnn0n0nn  12577  geolim  13938  geolim2  13939  georeclim  13940  geoisumr  13946  geoisum1c  13948  ramtcl2  14978  ramtcl2OLD  14979  lhop1  22978  logdmn0  23597  logcnlem3  23601  rusgranumwlkl1  25687  vcoprne  26210  strlem1  27915  subfacp1lem1  29914  rankeq1o  30950  poimirlem9  31961  poimirlem18  31970  poimirlem19  31971  poimirlem20  31972  poimirlem32  31984  fouriersw  38105  afvvfveq  38660  nn0nepnf  39089
  Copyright terms: Public domain W3C validator