Theorem necon3i 2956

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

Syntax hints:   → wi 4   = wceq 1624   ≠ wne 2924

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 197  df-ne 2925

This theorem is referenced by:  difn0  4078  xpnz  5703  unixp  5821  inf3lem2  8691  infeq5  8699  cantnflem1  8751  iunfictbso  9119  rankcf  9783  hashfun  13408  hashge3el3dif  13452  s1nzOLD  13570  abssubne0  14247  expnprm  15800  grpn0  17647  pmtr3ncomlem2  18086  pgpfaclem2  18673  isdrng2  18951  mpfrcl  19712  ply1frcl  19877  gzrngunit  20006  zringunit  20030  prmirredlem  20035  uvcf1  20325  lindfrn  20354  dfac14lem  21614  flimclslem  21981  lebnumlem3  22955  pmltpclem2  23410  i1fmullem  23652  fta1glem1  24116  fta1blem  24119  dgrcolem1  24220  plydivlem4  24242  plyrem  24251  facth  24252  fta1lem  24253  vieta1lem1  24256  vieta1lem2  24257  vieta1  24258  aalioulem2  24279  geolim3  24285  logcj  24543  argregt0  24547  argimgt0  24549  argimlt0  24550  logneg2  24552  tanarg  24556  logtayl  24597  cxpsqrt  24640  cxpcn3lem  24679  cxpcn3  24680  dcubic2  24762  dcubic  24764  cubic  24767  asinlem  24786  atandmcj  24827  atancj  24828  atanlogsublem  24833  bndatandm  24847  birthdaylem1  24869  basellem4  25001  basellem5  25002  dchrn0  25166  lgsne0  25251  usgr2trlncl  26858  nmlno0lem  27949  nmlnop0iALT  29155  cntnevol  30592  signsvtn0  30948  signstfveq0a  30954  signstfveq0  30955  nepss  31898  elima4  31976  heicant  33749  totbndbnd  33893  cdleme3c  36012  cdleme7e  36029  imadisjlnd  38953  compne  39137  compneOLD  39138  stoweidlem39  40751