Theorem necon3i 2993

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

Syntax hints:   → wi 4   = wceq 1507   ≠ wne 2961

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 199  df-ne 2962

This theorem is referenced by:  difn0  4204  xpnz  5850  unixp  5965  inf3lem2  8880  infeq5  8888  cantnflem1  8940  iunfictbso  9328  rankcf  9991  hashfun  13605  hashge3el3dif  13649  abssubne0  14531  expnprm  16088  grpn0  17917  pmtr3ncomlem2  18357  pgpfaclem2  18948  isdrng2  19229  mpfrcl  20005  ply1frcl  20178  gzrngunit  20307  zringunit  20331  prmirredlem  20336  uvcf1  20632  lindfrn  20661  dfac14lem  21923  flimclslem  22290  lebnumlem3  23264  pmltpclem2  23747  i1fmullem  23992  fta1glem1  24456  fta1blem  24459  dgrcolem1  24560  plydivlem4  24582  plyrem  24591  facth  24592  fta1lem  24593  vieta1lem1  24596  vieta1lem2  24597  vieta1  24598  aalioulem2  24619  geolim3  24625  logcj  24884  argregt0  24888  argimgt0  24890  argimlt0  24891  logneg2  24893  tanarg  24897  logtayl  24938  cxpsqrt  24981  cxpcn3lem  25023  cxpcn3  25024  dcubic2  25117  dcubic  25119  cubic  25122  asinlem  25141  atandmcj  25182  atancj  25183  atanlogsublem  25188  bndatandm  25202  birthdaylem1  25225  basellem4  25357  dchrn0  25522  lgsne0  25607  usgr2trlncl  27243  nmlno0lem  28341  nmlnop0iALT  29547  preimane  30171  cntnevol  31132  signsvtn0  31486  signsvtn0OLD  31487  signstfveq0a  31493  signstfveq0  31494  signstfveq0OLD  31495  nepss  32468  elima4  32539  heicant  34368  totbndbnd  34509  cdleme3c  36811  cdleme7e  36828  imadisjlnd  39874  compne  40191  compneOLD  40192  stoweidlem39  41755  rrx2vlinest  44096  rrx2linesl  44098