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 1543   ≠ 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 210  df-ne 2941

This theorem is referenced by:  difn0  4279  xpnz  6022  unixp  6145  inf3lem2  9244  infeq5  9252  cantnflem1  9304  iunfictbso  9728  rankcf  10391  hashfun  14004  hashge3el3dif  14052  abssubne0  14880  expnprm  16455  grpn0  18399  pmtr3ncomlem2  18866  pgpfaclem2  19469  isdrng2  19777  gzrngunit  20429  zringunit  20453  prmirredlem  20459  uvcf1  20754  lindfrn  20783  mpfrcl  21045  ply1frcl  21234  dfac14lem  22514  flimclslem  22881  lebnumlem3  23860  pmltpclem2  24346  i1fmullem  24591  fta1glem1  25063  fta1blem  25066  dgrcolem1  25167  plydivlem4  25189  plyrem  25198  facth  25199  fta1lem  25200  vieta1lem1  25203  vieta1lem2  25204  vieta1  25205  aalioulem2  25226  geolim3  25232  logcj  25494  argregt0  25498  argimgt0  25500  argimlt0  25501  logneg2  25503  tanarg  25507  logtayl  25548  cxpsqrt  25591  cxpcn3lem  25633  cxpcn3  25634  dcubic2  25727  dcubic  25729  cubic  25732  asinlem  25751  atandmcj  25792  atancj  25793  atanlogsublem  25798  bndatandm  25812  birthdaylem1  25834  basellem4  25966  dchrn0  26131  lgsne0  26216  usgr2trlncl  27847  nmlno0lem  28874  nmlnop0iALT  30076  eldmne0  30682  preimane  30727  prmidl0  31340  cntnevol  31908  signsvtn0  32261  signstfveq0a  32267  signstfveq0  32268  nepss  33377  elima4  33469  heicant  35549  totbndbnd  35684  cdleme3c  37981  cdleme7e  37998  uvcn0  39977  sn-1ne2  40002  sn-0ne2  40097  imadisjlnd  41448  compne  41732  stoweidlem39  43255  rrx2vlinest  45760  rrx2linesl  45762  elfvne0  45849