Theorem necon3i 2957

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

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

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 2926

This theorem is referenced by:  difn0  4326  imadisjlnd  6041  xpnz  6120  unixp  6243  inf3lem2  9558  infeq5  9566  cantnflem1  9618  iunfictbso  10043  rankcf  10706  hashfun  14378  hashge3el3dif  14428  abssubne0  15259  expnprm  16849  grpn0  18879  pmtr3ncomlem2  19380  pgpfaclem2  19990  isdrng2  20628  gzrngunit  21326  zringunit  21352  prmirredlem  21358  uvcf1  21677  lindfrn  21706  mpfrcl  21968  ply1frcl  22181  dfac14lem  23480  flimclslem  23847  lebnumlem3  24838  pmltpclem2  25326  i1fmullem  25571  fta1glem1  26049  fta1blem  26052  dgrcolem1  26155  plydivlem4  26180  plyrem  26189  facth  26190  fta1lem  26191  vieta1lem1  26194  vieta1lem2  26195  vieta1  26196  aalioulem2  26217  geolim3  26223  logcj  26491  argregt0  26495  argimgt0  26497  argimlt0  26498  logneg2  26500  tanarg  26504  logtayl  26545  cxpsqrt  26588  cxpcn3lem  26633  cxpcn3  26634  dcubic2  26730  dcubic  26732  cubic  26735  asinlem  26754  atandmcj  26795  atancj  26796  atanlogsublem  26801  bndatandm  26815  birthdaylem1  26837  basellem4  26970  dchrn0  27137  lgsne0  27222  usgr2trlncl  29663  nmlno0lem  30695  nmlnop0iALT  31897  eldmne0  32525  preimane  32567  prmidl0  33394  constrrtll  33694  cntnevol  34191  signsvtn0  34534  signstfveq0a  34540  signstfveq0  34541  nepss  35678  elima4  35736  heicant  37622  totbndbnd  37756  cdleme3c  40197  cdleme7e  40214  sn-1ne2  42226  sn-0ne2  42367  uvcn0  42503  compne  44403  stoweidlem39  46010  sinnpoly  46865  rrx2vlinest  48703  rrx2linesl  48705  elfvne0  48810  lanrcl  49583  ranrcl  49584  rellan  49585  relran  49586