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

Theorem necon2ai 2574
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 2533 . . 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 1647    =/= wne 2529
This theorem is referenced by:  necon2i  2576  neneqad  2599  intex  4269  iin0  4286  opelopabsb  4378  0ellim  4557  inf3lem3  7478  cardmin2  7778  pm54.43  7780  canthp1lem2  8422  renepnf  9026  renemnf  9027  lt0ne0d  9485  nnne0  9925  hashnemnf  11515  hashnn0n0nn  11551  geolim  12534  geolim2  12535  georeclim  12536  geoisumr  12542  geoisum1c  12544  ramtcl2  13266  lhop1  19576  logdmn0  20209  logcnlem3  20213  vcoprne  21448  strlem1  23143  subfacp1lem1  24313  rankeq1o  25543  afvvfveq  27519
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 2531
  Copyright terms: Public domain W3C validator