Theorem necon3i 2991

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  difn0  4318  imadisjlnd  6096  xpnz  6168  unixp  6309  inf3lem2  9667  infeq5  9675  cantnflem1  9727  iunfictbso  10232  rankcf  10901  hashfun  14623  hashge3el3dif  14673  abssubne0  15527  expnprm  17124  grpn0  19232  pmtr3ncomlem2  19739  pgpfaclem2  20349  isdrng2  21048  prmidl0  21685  gzrngunit  21793  zringunit  21827  prmirredlem  21833  uvcf1  22153  lindfrn  22182  mpfrcl  22449  ply1frcl  22691  dfac14lem  23991  flimclslem  24358  lebnumlem3  25339  pmltpclem2  25825  i1fmullem  26070  fta1glem1  26541  fta1blem  26544  dgrcolem1  26647  plydivlem4  26672  plyrem  26681  facth  26682  fta1lem  26683  vieta1lem1  26688  vieta1lem2  26689  vieta1  26690  aalioulem2  26717  geolim3  26723  logcj  26991  argregt0  26995  argimgt0  26997  argimlt0  26998  logneg2  27000  tanarg  27004  logtayl  27045  cxpsqrt  27088  cxpcn3lem  27132  cxpcn3  27133  dcubic2  27229  dcubic  27231  cubic  27234  asinlem  27253  atandmcj  27294  atancj  27295  atanlogsublem  27300  bndatandm  27314  birthdaylem1  27336  basellem4  27468  dchrn0  27634  lgsne0  27719  usgr2trlncl  30403  nmlno0lem  31452  nmlnop0iALT  32654  eldmne0  33319  preimane  33361  ricnzr1  33948  psrnzr  34255  constrrtll  34474  cntnevol  34972  signsvtn0  35310  signstfveq0a  35316  signstfveq0  35317  nepss  36698  elima4  36755  dfttc4lem2  37532  heicant  38841  totbndbnd  38989  cdleme3c  41553  cdleme7e  41570  sn-1ne2  43596  sn-0ne2  43723  uvcn0  43872  compne  45684  stoweidlem39  47322  sinnpoly  48214  rrx2vlinest  50184  rrx2linesl  50186  elfvne0  50291  fuconuniqlem  51112  lanrcl  51135  ranrcl  51136  rellan  51137  relran  51138