Theorem necon3i 2973

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

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

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 2941

This theorem is referenced by:  difn0  4367  imadisjlnd  6099  xpnz  6179  unixp  6302  inf3lem2  9669  infeq5  9677  cantnflem1  9729  iunfictbso  10154  rankcf  10817  hashfun  14476  hashge3el3dif  14526  abssubne0  15355  expnprm  16940  grpn0  18989  pmtr3ncomlem2  19492  pgpfaclem2  20102  isdrng2  20743  gzrngunit  21451  zringunit  21477  prmirredlem  21483  uvcf1  21812  lindfrn  21841  mpfrcl  22109  ply1frcl  22322  dfac14lem  23625  flimclslem  23992  lebnumlem3  24995  pmltpclem2  25484  i1fmullem  25729  fta1glem1  26207  fta1blem  26210  dgrcolem1  26313  plydivlem4  26338  plyrem  26347  facth  26348  fta1lem  26349  vieta1lem1  26352  vieta1lem2  26353  vieta1  26354  aalioulem2  26375  geolim3  26381  logcj  26648  argregt0  26652  argimgt0  26654  argimlt0  26655  logneg2  26657  tanarg  26661  logtayl  26702  cxpsqrt  26745  cxpcn3lem  26790  cxpcn3  26791  dcubic2  26887  dcubic  26889  cubic  26892  asinlem  26911  atandmcj  26952  atancj  26953  atanlogsublem  26958  bndatandm  26972  birthdaylem1  26994  basellem4  27127  dchrn0  27294  lgsne0  27379  usgr2trlncl  29780  nmlno0lem  30812  nmlnop0iALT  32014  eldmne0  32638  preimane  32680  prmidl0  33478  constrrtll  33772  cntnevol  34229  signsvtn0  34585  signstfveq0a  34591  signstfveq0  34592  nepss  35718  elima4  35776  heicant  37662  totbndbnd  37796  cdleme3c  40232  cdleme7e  40249  sn-1ne2  42300  sn-0ne2  42436  uvcn0  42552  compne  44460  stoweidlem39  46054  rrx2vlinest  48662  rrx2linesl  48664  elfvne0  48758