Theorem necon3i 2961

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  difn0  4316  imadisjlnd  6037  xpnz  6114  unixp  6237  inf3lem2  9530  infeq5  9538  cantnflem1  9590  iunfictbso  10016  rankcf  10679  hashfun  14351  hashge3el3dif  14401  abssubne0  15231  expnprm  16821  grpn0  18892  pmtr3ncomlem2  19394  pgpfaclem2  20004  isdrng2  20667  gzrngunit  21379  zringunit  21412  prmirredlem  21418  uvcf1  21738  lindfrn  21767  mpfrcl  22031  ply1frcl  22253  dfac14lem  23552  flimclslem  23919  lebnumlem3  24909  pmltpclem2  25397  i1fmullem  25642  fta1glem1  26120  fta1blem  26123  dgrcolem1  26226  plydivlem4  26251  plyrem  26260  facth  26261  fta1lem  26262  vieta1lem1  26265  vieta1lem2  26266  vieta1  26267  aalioulem2  26288  geolim3  26294  logcj  26562  argregt0  26566  argimgt0  26568  argimlt0  26569  logneg2  26571  tanarg  26575  logtayl  26616  cxpsqrt  26659  cxpcn3lem  26704  cxpcn3  26705  dcubic2  26801  dcubic  26803  cubic  26806  asinlem  26825  atandmcj  26866  atancj  26867  atanlogsublem  26872  bndatandm  26886  birthdaylem1  26908  basellem4  27041  dchrn0  27208  lgsne0  27293  usgr2trlncl  29759  nmlno0lem  30794  nmlnop0iALT  31996  eldmne0  32631  preimane  32674  prmidl0  33459  constrrtll  33816  cntnevol  34313  signsvtn0  34655  signstfveq0a  34661  signstfveq0  34662  nepss  35834  elima4  35892  heicant  37768  totbndbnd  37902  cdleme3c  40402  cdleme7e  40419  sn-1ne2  42435  sn-0ne2  42576  uvcn0  42712  compne  44597  stoweidlem39  46199  sinnpoly  47053  rrx2vlinest  48903  rrx2linesl  48905  elfvne0  49010  lanrcl  49782  ranrcl  49783  rellan  49784  relran  49785