Theorem necon3i 2974

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

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

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 206  df-ne 2942

This theorem is referenced by:  difn0  4365  xpnz  6159  unixp  6282  inf3lem2  9624  infeq5  9632  cantnflem1  9684  iunfictbso  10109  rankcf  10772  hashfun  14397  hashge3el3dif  14447  abssubne0  15263  expnprm  16835  grpn0  18856  pmtr3ncomlem2  19342  pgpfaclem2  19952  isdrng2  20371  gzrngunit  21011  zringunit  21036  prmirredlem  21042  uvcf1  21347  lindfrn  21376  mpfrcl  21648  ply1frcl  21837  dfac14lem  23121  flimclslem  23488  lebnumlem3  24479  pmltpclem2  24966  i1fmullem  25211  fta1glem1  25683  fta1blem  25686  dgrcolem1  25787  plydivlem4  25809  plyrem  25818  facth  25819  fta1lem  25820  vieta1lem1  25823  vieta1lem2  25824  vieta1  25825  aalioulem2  25846  geolim3  25852  logcj  26114  argregt0  26118  argimgt0  26120  argimlt0  26121  logneg2  26123  tanarg  26127  logtayl  26168  cxpsqrt  26211  cxpcn3lem  26255  cxpcn3  26256  dcubic2  26349  dcubic  26351  cubic  26354  asinlem  26373  atandmcj  26414  atancj  26415  atanlogsublem  26420  bndatandm  26434  birthdaylem1  26456  basellem4  26588  dchrn0  26753  lgsne0  26838  usgr2trlncl  29017  nmlno0lem  30046  nmlnop0iALT  31248  eldmne0  31852  preimane  31895  prmidl0  32569  cntnevol  33226  signsvtn0  33581  signstfveq0a  33587  signstfveq0  33588  nepss  34687  elima4  34747  heicant  36523  totbndbnd  36657  cdleme3c  39101  cdleme7e  39118  uvcn0  41112  sn-1ne2  41179  sn-0ne2  41279  imadisjlnd  42912  compne  43200  stoweidlem39  44755  rrx2vlinest  47427  rrx2linesl  47429  elfvne0  47515