MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3i Structured version   Visualization version   GIF version

Theorem necon3i 2975
Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon3i.1 (𝐴 = 𝐵𝐶 = 𝐷)
Assertion
Ref Expression
necon3i (𝐶𝐷𝐴𝐵)

Proof of Theorem necon3i
StepHypRef Expression
1 necon3i.1 . . 3 (𝐴 = 𝐵𝐶 = 𝐷)
21necon3ai 2968 . 2 (𝐶𝐷 → ¬ 𝐴 = 𝐵)
32neqned 2950 1 (𝐶𝐷𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wne 2943
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 197  df-ne 2944
This theorem is referenced by:  difn0  4091  xpnz  5693  unixp  5811  inf3lem2  8694  infeq5  8702  cantnflem1  8754  iunfictbso  9141  rankcf  9805  hashfun  13426  hashge3el3dif  13470  abssubne0  14264  expnprm  15813  grpn0  17662  pmtr3ncomlem2  18101  pgpfaclem2  18689  isdrng2  18967  mpfrcl  19733  ply1frcl  19898  gzrngunit  20027  zringunit  20051  prmirredlem  20056  uvcf1  20348  lindfrn  20377  dfac14lem  21641  flimclslem  22008  lebnumlem3  22982  pmltpclem2  23437  i1fmullem  23681  fta1glem1  24145  fta1blem  24148  dgrcolem1  24249  plydivlem4  24271  plyrem  24280  facth  24281  fta1lem  24282  vieta1lem1  24285  vieta1lem2  24286  vieta1  24287  aalioulem2  24308  geolim3  24314  logcj  24573  argregt0  24577  argimgt0  24579  argimlt0  24580  logneg2  24582  tanarg  24586  logtayl  24627  cxpsqrt  24670  cxpcn3lem  24709  cxpcn3  24710  dcubic2  24792  dcubic  24794  cubic  24797  asinlem  24816  atandmcj  24857  atancj  24858  atanlogsublem  24863  bndatandm  24877  birthdaylem1  24899  basellem4  25031  basellem5  25032  dchrn0  25196  lgsne0  25281  usgr2trlncl  26891  nmlno0lem  27988  nmlnop0iALT  29194  cntnevol  30631  signsvtn0  30987  signstfveq0a  30993  signstfveq0  30994  nepss  31937  elima4  32015  heicant  33776  totbndbnd  33918  cdleme3c  36038  cdleme7e  36055  imadisjlnd  38983  compne  39167  compneOLD  39168  stoweidlem39  40768
  Copyright terms: Public domain W3C validator