Theorem necon3i 2969

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

Syntax hints:   → wi 4   = wceq 1652   ≠ wne 2937

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 198  df-ne 2938

This theorem is referenced by:  difn0  4107  xpnz  5736  unixp  5854  inf3lem2  8741  infeq5  8749  cantnflem1  8801  iunfictbso  9188  rankcf  9852  hashfun  13425  hashge3el3dif  13469  abssubne0  14343  expnprm  15887  grpn0  17723  pmtr3ncomlem2  18159  pgpfaclem2  18748  isdrng2  19026  mpfrcl  19791  ply1frcl  19956  gzrngunit  20085  zringunit  20109  prmirredlem  20114  uvcf1  20407  lindfrn  20436  dfac14lem  21700  flimclslem  22067  lebnumlem3  23041  pmltpclem2  23507  i1fmullem  23752  fta1glem1  24216  fta1blem  24219  dgrcolem1  24320  plydivlem4  24342  plyrem  24351  facth  24352  fta1lem  24353  vieta1lem1  24356  vieta1lem2  24357  vieta1  24358  aalioulem2  24379  geolim3  24385  logcj  24643  argregt0  24647  argimgt0  24649  argimlt0  24650  logneg2  24652  tanarg  24656  logtayl  24697  cxpsqrt  24740  cxpcn3lem  24779  cxpcn3  24780  dcubic2  24862  dcubic  24864  cubic  24867  asinlem  24886  atandmcj  24927  atancj  24928  atanlogsublem  24933  bndatandm  24947  birthdaylem1  24969  basellem4  25101  basellem5  25102  dchrn0  25266  lgsne0  25351  usgr2trlncl  26947  nmlno0lem  28039  nmlnop0iALT  29245  cntnevol  30673  signsvtn0  31030  signstfveq0a  31036  signstfveq0  31037  nepss  31977  elima4  32054  heicant  33800  totbndbnd  33942  cdleme3c  36118  cdleme7e  36135  imadisjlnd  39065  compne  39248  compneOLD  39249  stoweidlem39  40825