Theorem necon3i 2965

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 2958	. 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵)
3	2	neqned 2940	1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)

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

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 2934

This theorem is referenced by:  difn0  4321  imadisjlnd  6048  xpnz  6125  unixp  6248  inf3lem2  9550  infeq5  9558  cantnflem1  9610  iunfictbso  10036  rankcf  10700  hashfun  14372  hashge3el3dif  14422  abssubne0  15252  expnprm  16842  grpn0  18913  pmtr3ncomlem2  19415  pgpfaclem2  20025  isdrng2  20688  gzrngunit  21400  zringunit  21433  prmirredlem  21439  uvcf1  21759  lindfrn  21788  mpfrcl  22052  ply1frcl  22274  dfac14lem  23573  flimclslem  23940  lebnumlem3  24930  pmltpclem2  25418  i1fmullem  25663  fta1glem1  26141  fta1blem  26144  dgrcolem1  26247  plydivlem4  26272  plyrem  26281  facth  26282  fta1lem  26283  vieta1lem1  26286  vieta1lem2  26287  vieta1  26288  aalioulem2  26309  geolim3  26315  logcj  26583  argregt0  26587  argimgt0  26589  argimlt0  26590  logneg2  26592  tanarg  26596  logtayl  26637  cxpsqrt  26680  cxpcn3lem  26725  cxpcn3  26726  dcubic2  26822  dcubic  26824  cubic  26827  asinlem  26846  atandmcj  26887  atancj  26888  atanlogsublem  26893  bndatandm  26907  birthdaylem1  26929  basellem4  27062  dchrn0  27229  lgsne0  27314  usgr2trlncl  29845  nmlno0lem  30881  nmlnop0iALT  32083  eldmne0  32717  preimane  32759  prmidl0  33543  constrrtll  33909  cntnevol  34406  signsvtn0  34748  signstfveq0a  34754  signstfveq0  34755  nepss  35934  elima4  35992  heicant  37906  totbndbnd  38040  cdleme3c  40606  cdleme7e  40623  sn-1ne2  42635  sn-0ne2  42776  uvcn0  42912  compne  44796  stoweidlem39  46397  sinnpoly  47251  rrx2vlinest  49101  rrx2linesl  49103  elfvne0  49208  lanrcl  49980  ranrcl  49981  rellan  49982  relran  49983