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

Theorem necon2ai 2491
Description: Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon2ai.1  |-  ( A  =  B  ->  -.  ph )
Assertion
Ref Expression
necon2ai  |-  ( ph  ->  A  =/=  B )

Proof of Theorem necon2ai
StepHypRef Expression
1 nne 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon2ai.1 . . 3  |-  ( A  =  B  ->  -.  ph )
31, 2sylbi 187 . 2  |-  ( -.  A  =/=  B  ->  -.  ph )
43con4i 122 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon2i  2493  neneqad  2516  intex  4167  iin0  4184  opelopabsb  4275  0ellim  4454  inf3lem3  7331  cardmin2  7631  pm54.43  7633  canthp1lem2  8275  renepnf  8879  renemnf  8880  lt0ne0d  9338  nnne0  9778  geolim  12326  geolim2  12327  georeclim  12328  geoisumr  12334  geoisum1c  12336  ramtcl2  13058  lhop1  19361  logdmn0  19987  logcnlem3  19991  vcoprne  21135  strlem1  22830  subfacp1lem1  23710  funpartfv  24483  rankeq1o  24801  afvvfveq  28011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2448
  Copyright terms: Public domain W3C validator