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 1541   ≠ 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  4319  imadisjlnd  6040  xpnz  6117  unixp  6240  inf3lem2  9538  infeq5  9546  cantnflem1  9598  iunfictbso  10024  rankcf  10688  hashfun  14360  hashge3el3dif  14410  abssubne0  15240  expnprm  16830  grpn0  18901  pmtr3ncomlem2  19403  pgpfaclem2  20013  isdrng2  20676  gzrngunit  21388  zringunit  21421  prmirredlem  21427  uvcf1  21747  lindfrn  21776  mpfrcl  22040  ply1frcl  22262  dfac14lem  23561  flimclslem  23928  lebnumlem3  24918  pmltpclem2  25406  i1fmullem  25651  fta1glem1  26129  fta1blem  26132  dgrcolem1  26235  plydivlem4  26260  plyrem  26269  facth  26270  fta1lem  26271  vieta1lem1  26274  vieta1lem2  26275  vieta1  26276  aalioulem2  26297  geolim3  26303  logcj  26571  argregt0  26575  argimgt0  26577  argimlt0  26578  logneg2  26580  tanarg  26584  logtayl  26625  cxpsqrt  26668  cxpcn3lem  26713  cxpcn3  26714  dcubic2  26810  dcubic  26812  cubic  26815  asinlem  26834  atandmcj  26875  atancj  26876  atanlogsublem  26881  bndatandm  26895  birthdaylem1  26917  basellem4  27050  dchrn0  27217  lgsne0  27302  usgr2trlncl  29833  nmlno0lem  30868  nmlnop0iALT  32070  eldmne0  32705  preimane  32748  prmidl0  33531  constrrtll  33888  cntnevol  34385  signsvtn0  34727  signstfveq0a  34733  signstfveq0  34734  nepss  35912  elima4  35970  heicant  37856  totbndbnd  37990  cdleme3c  40490  cdleme7e  40507  sn-1ne2  42520  sn-0ne2  42661  uvcn0  42797  compne  44681  stoweidlem39  46283  sinnpoly  47137  rrx2vlinest  48987  rrx2linesl  48989  elfvne0  49094  lanrcl  49866  ranrcl  49867  rellan  49868  relran  49869