Theorem necon3i 2972

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

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

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 206  df-ne 2940

This theorem is referenced by:  difn0  4329  xpnz  6116  unixp  6239  inf3lem2  9574  infeq5  9582  cantnflem1  9634  iunfictbso  10059  rankcf  10722  hashfun  14347  hashge3el3dif  14397  abssubne0  15213  expnprm  16785  grpn0  18796  pmtr3ncomlem2  19270  pgpfaclem2  19875  isdrng2  20238  gzrngunit  20900  zringunit  20924  prmirredlem  20930  uvcf1  21235  lindfrn  21264  mpfrcl  21532  ply1frcl  21721  dfac14lem  23005  flimclslem  23372  lebnumlem3  24363  pmltpclem2  24850  i1fmullem  25095  fta1glem1  25567  fta1blem  25570  dgrcolem1  25671  plydivlem4  25693  plyrem  25702  facth  25703  fta1lem  25704  vieta1lem1  25707  vieta1lem2  25708  vieta1  25709  aalioulem2  25730  geolim3  25736  logcj  25998  argregt0  26002  argimgt0  26004  argimlt0  26005  logneg2  26007  tanarg  26011  logtayl  26052  cxpsqrt  26095  cxpcn3lem  26137  cxpcn3  26138  dcubic2  26231  dcubic  26233  cubic  26236  asinlem  26255  atandmcj  26296  atancj  26297  atanlogsublem  26302  bndatandm  26316  birthdaylem1  26338  basellem4  26470  dchrn0  26635  lgsne0  26720  usgr2trlncl  28771  nmlno0lem  29798  nmlnop0iALT  31000  eldmne0  31609  preimane  31653  prmidl0  32299  cntnevol  32916  signsvtn0  33271  signstfveq0a  33277  signstfveq0  33278  nepss  34376  elima4  34436  heicant  36186  totbndbnd  36321  cdleme3c  38766  cdleme7e  38783  uvcn0  40788  sn-1ne2  40839  sn-0ne2  40933  imadisjlnd  42555  compne  42843  stoweidlem39  44400  rrx2vlinest  46947  rrx2linesl  46949  elfvne0  47035