Theorem necon3i 2964

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

Step	Hyp	Ref	Expression
1		necon3i.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)
2	1	necon3ai 2957	. 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵)
3	2	neqned 2939	1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  difn0  4307  imadisjlnd  6046  xpnz  6123  unixp  6246  inf3lem2  9550  infeq5  9558  cantnflem1  9610  iunfictbso  10036  rankcf  10700  hashfun  14399  hashge3el3dif  14449  abssubne0  15279  expnprm  16873  grpn0  18947  pmtr3ncomlem2  19449  pgpfaclem2  20059  isdrng2  20720  gzrngunit  21413  zringunit  21446  prmirredlem  21452  uvcf1  21772  lindfrn  21801  mpfrcl  22063  ply1frcl  22283  dfac14lem  23582  flimclslem  23949  lebnumlem3  24930  pmltpclem2  25416  i1fmullem  25661  fta1glem1  26133  fta1blem  26136  dgrcolem1  26238  plydivlem4  26262  plyrem  26271  facth  26272  fta1lem  26273  vieta1lem1  26276  vieta1lem2  26277  vieta1  26278  aalioulem2  26299  geolim3  26305  logcj  26570  argregt0  26574  argimgt0  26576  argimlt0  26577  logneg2  26579  tanarg  26583  logtayl  26624  cxpsqrt  26667  cxpcn3lem  26711  cxpcn3  26712  dcubic2  26808  dcubic  26810  cubic  26813  asinlem  26832  atandmcj  26873  atancj  26874  atanlogsublem  26879  bndatandm  26893  birthdaylem1  26915  basellem4  27047  dchrn0  27213  lgsne0  27298  usgr2trlncl  29828  nmlno0lem  30864  nmlnop0iALT  32066  eldmne0  32700  preimane  32742  prmidl0  33510  constrrtll  33875  cntnevol  34372  signsvtn0  34714  signstfveq0a  34720  signstfveq0  34721  nepss  35900  elima4  35958  dfttc4lem2  36711  heicant  37976  totbndbnd  38110  cdleme3c  40676  cdleme7e  40693  sn-1ne2  42703  sn-0ne2  42838  uvcn0  42987  compne  44867  stoweidlem39  46467  sinnpoly  47339  rrx2vlinest  49217  rrx2linesl  49219  elfvne0  49324  lanrcl  50096  ranrcl  50097  rellan  50098  relran  50099