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

Theorem necon2ai 2638
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 2606 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1405    =/= wne 2598
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 2600
This theorem is referenced by:  necon2i  2646  neneqadOLD  2712  intex  4549  iin0  4567  opelopabsb  4699  0ellim  5471  inf3lem3  8079  cardmin2  8410  pm54.43  8412  canthp1lem2  9060  renepnf  9670  renemnf  9671  lt0ne0d  10157  nnne0  10608  hashnemnf  12462  hashnn0n0nn  12505  geolim  13829  geolim2  13830  georeclim  13831  geoisumr  13837  geoisum1c  13839  ramtcl2  14736  lhop1  22705  logdmn0  23313  logcnlem3  23317  rusgranumwlkl1  25351  vcoprne  25872  strlem1  27568  subfacp1lem1  29463  rankeq1o  30496  fouriersw  37363  afvvfveq  37582
  Copyright terms: Public domain W3C validator