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  4330  imadisjlnd  6052  xpnz  6132  unixp  6255  inf3lem2  9582  infeq5  9590  cantnflem1  9642  iunfictbso  10067  rankcf  10730  hashfun  14402  hashge3el3dif  14452  abssubne0  15283  expnprm  16873  grpn0  18903  pmtr3ncomlem2  19404  pgpfaclem2  20014  isdrng2  20652  gzrngunit  21350  zringunit  21376  prmirredlem  21382  uvcf1  21701  lindfrn  21730  mpfrcl  21992  ply1frcl  22205  dfac14lem  23504  flimclslem  23871  lebnumlem3  24862  pmltpclem2  25350  i1fmullem  25595  fta1glem1  26073  fta1blem  26076  dgrcolem1  26179  plydivlem4  26204  plyrem  26213  facth  26214  fta1lem  26215  vieta1lem1  26218  vieta1lem2  26219  vieta1  26220  aalioulem2  26241  geolim3  26247  logcj  26515  argregt0  26519  argimgt0  26521  argimlt0  26522  logneg2  26524  tanarg  26528  logtayl  26569  cxpsqrt  26612  cxpcn3lem  26657  cxpcn3  26658  dcubic2  26754  dcubic  26756  cubic  26759  asinlem  26778  atandmcj  26819  atancj  26820  atanlogsublem  26825  bndatandm  26839  birthdaylem1  26861  basellem4  26994  dchrn0  27161  lgsne0  27246  usgr2trlncl  29690  nmlno0lem  30722  nmlnop0iALT  31924  eldmne0  32552  preimane  32594  prmidl0  33421  constrrtll  33721  cntnevol  34218  signsvtn0  34561  signstfveq0a  34567  signstfveq0  34568  nepss  35705  elima4  35763  heicant  37649  totbndbnd  37783  cdleme3c  40224  cdleme7e  40241  sn-1ne2  42253  sn-0ne2  42394  uvcn0  42530  compne  44430  stoweidlem39  46037  sinnpoly  46892  rrx2vlinest  48730  rrx2linesl  48732  elfvne0  48837  lanrcl  49610  ranrcl  49611  rellan  49612  relran  49613