Theorem necon3i 2958

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  difn0  4333  imadisjlnd  6055  xpnz  6135  unixp  6258  inf3lem2  9589  infeq5  9597  cantnflem1  9649  iunfictbso  10074  rankcf  10737  hashfun  14409  hashge3el3dif  14459  abssubne0  15290  expnprm  16880  grpn0  18910  pmtr3ncomlem2  19411  pgpfaclem2  20021  isdrng2  20659  gzrngunit  21357  zringunit  21383  prmirredlem  21389  uvcf1  21708  lindfrn  21737  mpfrcl  21999  ply1frcl  22212  dfac14lem  23511  flimclslem  23878  lebnumlem3  24869  pmltpclem2  25357  i1fmullem  25602  fta1glem1  26080  fta1blem  26083  dgrcolem1  26186  plydivlem4  26211  plyrem  26220  facth  26221  fta1lem  26222  vieta1lem1  26225  vieta1lem2  26226  vieta1  26227  aalioulem2  26248  geolim3  26254  logcj  26522  argregt0  26526  argimgt0  26528  argimlt0  26529  logneg2  26531  tanarg  26535  logtayl  26576  cxpsqrt  26619  cxpcn3lem  26664  cxpcn3  26665  dcubic2  26761  dcubic  26763  cubic  26766  asinlem  26785  atandmcj  26826  atancj  26827  atanlogsublem  26832  bndatandm  26846  birthdaylem1  26868  basellem4  27001  dchrn0  27168  lgsne0  27253  usgr2trlncl  29697  nmlno0lem  30729  nmlnop0iALT  31931  eldmne0  32559  preimane  32601  prmidl0  33428  constrrtll  33728  cntnevol  34225  signsvtn0  34568  signstfveq0a  34574  signstfveq0  34575  nepss  35712  elima4  35770  heicant  37656  totbndbnd  37790  cdleme3c  40231  cdleme7e  40248  sn-1ne2  42260  sn-0ne2  42401  uvcn0  42537  compne  44437  stoweidlem39  46044  rrx2vlinest  48734  rrx2linesl  48736  elfvne0  48841  lanrcl  49614  ranrcl  49615  rellan  49616  relran  49617