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

Theorem necon3i 3019
 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 3012 . 2 (𝐶𝐷 → ¬ 𝐴 = 𝐵)
32neqned 2994 1 (𝐶𝐷𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2987 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 210  df-ne 2988 This theorem is referenced by:  difn0  4280  xpnz  5986  unixp  6106  inf3lem2  9091  infeq5  9099  cantnflem1  9151  iunfictbso  9540  rankcf  10203  hashfun  13811  hashge3el3dif  13857  abssubne0  14685  expnprm  16245  grpn0  18145  pmtr3ncomlem2  18612  pgpfaclem2  19215  isdrng2  19523  gzrngunit  20175  zringunit  20199  prmirredlem  20205  uvcf1  20500  lindfrn  20529  mpfrcl  20791  ply1frcl  20980  dfac14lem  22260  flimclslem  22627  lebnumlem3  23606  pmltpclem2  24091  i1fmullem  24336  fta1glem1  24807  fta1blem  24810  dgrcolem1  24911  plydivlem4  24933  plyrem  24942  facth  24943  fta1lem  24944  vieta1lem1  24947  vieta1lem2  24948  vieta1  24949  aalioulem2  24970  geolim3  24976  logcj  25238  argregt0  25242  argimgt0  25244  argimlt0  25245  logneg2  25247  tanarg  25251  logtayl  25292  cxpsqrt  25335  cxpcn3lem  25377  cxpcn3  25378  dcubic2  25471  dcubic  25473  cubic  25476  asinlem  25495  atandmcj  25536  atancj  25537  atanlogsublem  25542  bndatandm  25556  birthdaylem1  25578  basellem4  25710  dchrn0  25875  lgsne0  25960  usgr2trlncl  27590  nmlno0lem  28617  nmlnop0iALT  29819  eldmne0  30428  preimane  30474  prmidl0  31092  cntnevol  31660  signsvtn0  32013  signstfveq0a  32019  signstfveq0  32020  nepss  33124  elima4  33195  heicant  35159  totbndbnd  35294  cdleme3c  37593  cdleme7e  37610  sn-1ne2  39553  sn-0ne2  39631  imadisjlnd  40951  compne  41232  stoweidlem39  42765  rrx2vlinest  45237  rrx2linesl  45239
 Copyright terms: Public domain W3C validator