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 1539   ≠ 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  4304  xpnz  6077  unixp  6200  inf3lem2  9431  infeq5  9439  cantnflem1  9491  iunfictbso  9916  rankcf  10579  hashfun  14197  hashge3el3dif  14245  abssubne0  15073  expnprm  16648  grpn0  18656  pmtr3ncomlem2  19127  pgpfaclem2  19730  isdrng2  20046  gzrngunit  20709  zringunit  20733  prmirredlem  20739  uvcf1  21044  lindfrn  21073  mpfrcl  21340  ply1frcl  21529  dfac14lem  22813  flimclslem  23180  lebnumlem3  24171  pmltpclem2  24658  i1fmullem  24903  fta1glem1  25375  fta1blem  25378  dgrcolem1  25479  plydivlem4  25501  plyrem  25510  facth  25511  fta1lem  25512  vieta1lem1  25515  vieta1lem2  25516  vieta1  25517  aalioulem2  25538  geolim3  25544  logcj  25806  argregt0  25810  argimgt0  25812  argimlt0  25813  logneg2  25815  tanarg  25819  logtayl  25860  cxpsqrt  25903  cxpcn3lem  25945  cxpcn3  25946  dcubic2  26039  dcubic  26041  cubic  26044  asinlem  26063  atandmcj  26104  atancj  26105  atanlogsublem  26110  bndatandm  26124  birthdaylem1  26146  basellem4  26278  dchrn0  26443  lgsne0  26528  usgr2trlncl  28173  nmlno0lem  29200  nmlnop0iALT  30402  eldmne0  31008  preimane  31052  prmidl0  31671  cntnevol  32241  signsvtn0  32594  signstfveq0a  32600  signstfveq0  32601  nepss  33707  elima4  33795  heicant  35856  totbndbnd  35991  cdleme3c  38286  cdleme7e  38303  uvcn0  40302  sn-1ne2  40332  sn-0ne2  40426  imadisjlnd  41809  compne  42097  stoweidlem39  43629  rrx2vlinest  46145  rrx2linesl  46147  elfvne0  46234