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

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

Proof of Theorem necon3ai
StepHypRef Expression
1 necon3ai.1 . . 3  |-  ( ph  ->  A  =  B )
2 nne 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
31, 2sylibr 203 . 2  |-  ( ph  ->  -.  A  =/=  B
)
43con2i 112 1  |-  ( A  =/=  B  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  disjsn2  3694  opelopabsb  4275  0nelxp  4717  fvunsn  5712  map0b  6806  mapdom3  7033  wemapso2  7267  cflim2  7889  isfin4-3  7941  ac9  8110  ac9s  8120  fpwwe2lem13  8264  tskuni  8405  recextlem2  9399  hashprg  11368  eqsqr2d  11852  gcd1  12711  gcdeq  12731  phimullem  12847  pcgcd1  12929  pc2dvds  12931  pockthlem  12952  ablfacrplem  15300  lbsextlem4  15914  znrrg  16519  obslbs  16630  opnfbas  17537  supfil  17590  itg1addlem4  19054  itg1addlem5  19055  dvdsmulf1o  20434  ppiub  20443  dchrelbas4  20482  lgsne0  20572  2sqlem8  20611  derangsn  23701  subfacp1lem6  23716  cvmsss2  23805  vdgr1b  23895  neiopne  25051  fvsnn  25114  wallispi  27819  difprsng  28069  nbcusgra  28159  uvtxnbgra  28165  a9e2ndeq  28325
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