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

Theorem necon2ai 2651
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 2607 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon2ai.1 . . 3  |-  ( A  =  B  ->  -.  ph )
31, 2sylbi 189 . 2  |-  ( -.  A  =/=  B  ->  -.  ph )
43con4i 125 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon2i  2653  neneqad  2676  intex  4359  iin0  4376  opelopabsb  4468  0ellim  4646  inf3lem3  7588  cardmin2  7890  pm54.43  7892  canthp1lem2  8533  renepnf  9137  renemnf  9138  lt0ne0d  9597  nnne0  10037  hashnemnf  11633  hashnn0n0nn  11669  geolim  12652  geolim2  12653  georeclim  12654  geoisumr  12660  geoisum1c  12662  ramtcl2  13384  lhop1  19903  logdmn0  20536  logcnlem3  20540  vcoprne  22063  strlem1  23758  subfacp1lem1  24870  rankeq1o  26117  afvvfveq  28002
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator