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

Theorem necon2ai 2616
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 2575 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon2ai.1 . . 3  |-  ( A  =  B  ->  -.  ph )
31, 2sylbi 188 . 2  |-  ( -.  A  =/=  B  ->  -.  ph )
43con4i 124 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2571
This theorem is referenced by:  necon2i  2618  neneqad  2641  intex  4320  iin0  4337  opelopabsb  4429  0ellim  4607  inf3lem3  7545  cardmin2  7845  pm54.43  7847  canthp1lem2  8488  renepnf  9092  renemnf  9093  lt0ne0d  9552  nnne0  9992  hashnemnf  11587  hashnn0n0nn  11623  geolim  12606  geolim2  12607  georeclim  12608  geoisumr  12614  geoisum1c  12616  ramtcl2  13338  lhop1  19855  logdmn0  20488  logcnlem3  20492  vcoprne  22015  strlem1  23710  subfacp1lem1  24822  rankeq1o  26020  afvvfveq  27883
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 178  df-ne 2573
  Copyright terms: Public domain W3C validator