Theorem necon3d 2980

Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)

Hypothesis

Ref	Expression
necon3d.1	⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))

Assertion

Ref	Expression
necon3d	⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

Proof of Theorem necon3d

Step	Hyp	Ref	Expression
1		necon3d.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷))
2	1	necon3ad 2972	. 2 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵))
3		df-ne 2960	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 255	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  pssdifn0  4319  ssn0  4358  uniintsn  4948  funopsnOLD  7176  dff14i  7286  f1prex  7315  poxp3  8194  ressuppssdif  8230  suppfnss  8234  suppssov1  8242  suppssov2  8243  suppssfv  8247  omord  8604  nnmord  8669  mapdom2  9195  kmlem9  10264  isf32lem7  10464  1re  11335  addrid  11517  addn0nid  11763  nn0n0n1ge2  12701  xnegdi  13405  fseqsupubi  14148  sqrtgt0  15454  supcvg  16054  ntrivcvgfvn0  16097  efne0d  16292  efne0OLD  16294  divgcdcoprmex  16870  pceulem  17052  pcqmul  17060  pcqcl  17063  pcaddlem  17095  pcadd  17096  grpinvnz  19249  symgfvne  19625  symg2bas  19637  odmulgeq  19801  gsumval3lem2  20150  gsumval3  20151  ogrpaddlt  20382  ring1ne0  20560  ringelnzr  20804  0ringnnzr  20806  isdrng3lem2  21036  isdrng5  21038  abvdom  21117  lmodfopne  21205  mptscmfsupp0  21232  lmodindp1  21319  lspsneleq  21423  lspsneq  21430  lspexch  21437  lspindp3  21444  lspsnsubn0  21448  dsmmsubg  22079  dsmmlss  22080  elfrlmbasn0  22099  coe1tmmul2  22625  ply1scln0  22640  mavmulsolcl  22896  0ntr  23419  elcls3  23431  neindisj  23465  neindisj2  23471  conndisj  23764  dfconn2  23767  fbunfip  24218  deg1mul2  26462  ply1nzb  26471  ne0p  26555  dgreq0  26614  dgradd2  26617  dgrcolem2  26623  elqaalem3  26674  logcj  26964  argimgt0  26970  tanarg  26977  cxpsqrtth  27088  dvcnsqrt  27102  ang180lem2  27168  ftalem2  27431  ftalem4  27433  ftalem5  27434  dvdssqf  27495  cutbdaylt  28214  expsne0  28852  lmimid  29329  lmiisolem  29331  hypcgrlem1  29335  hypcgrlem2  29336  f1otrg  29478  f1otrge  29479  ax5seglem4  29540  ax5seglem5  29541  axeuclid  29571  axcontlem2  29573  axcontlem4  29575  pthdivtx  30342  spthdep  30350  usgr2wlkneq  30372  usgr2trlncl  30376  clwwlkccat  30611  clwwlkwwlksb  30675  clwwlknonel  30716  3pthdlem1  30795  uhgr3cyclexlem  30812  frgrwopreglem4a  30941  frrusgrord0lem  30970  nmlno0lem  31425  hlipgt0  31546  h1dn0  32184  spansneleq  32202  h1datomi  32213  nmlnop0iALT  32627  superpos  32986  chirredi  33026  preimane  33335  preiman0  33374  psgnfzto1stlem  33731  cycpmrn  33774  rmfsupp2  33868  pidlnzb  34042  drngidlhash  34053  extdgfialglem2  34395  constrsqrtcl  34481  qqhval2lem  34683  derangenlem  36103  subfacp1lem5  36116  btwndiff  36970  btwnconn1lem7  37036  btwnconn1lem12  37041  tan2h  38727  poimirlem1  38731  poimirlem9  38739  poimirlem17  38747  poimirlem22  38752  areacirclem1  38818  isdrngo2  39084  isdrngo3  39085  lsatn0  40248  lsatspn0  40249  lkrlspeqN  40420  cvlsupr2  40592  dalem25  40947  4atexlemcnd  41321  ltrncnvnid  41376  trlator0  41420  ltrnnidn  41423  trlnid  41428  cdleme3b  41478  cdleme11l  41518  cdleme16b  41528  cdleme35h2  41706  cdleme38n  41713  cdlemg8c  41878  cdlemg11a  41886  cdlemg12e  41896  cdlemg18a  41927  trlcoat  41972  trlcone  41977  tendo1ne0  42077  cdleml9  42233  dvheveccl  42361  dihmeetlem13N  42568  dihlspsnat  42582  dihpN  42585  dihatexv  42587  dochsat  42632  dochkrshp  42635  dochkr1  42727  lcfrlem28  42819  lcfrlem32  42823  mapdn0  42918  mapdpglem11  42931  mapdpglem16  42936  sticksstones1  43388  sn-1ne2  43523  pell1234qrne0  44053  jm2.26lem3  44201  2zrngnmlid  49557  2zrngnmrid  49558  2zrngnmlid2  49559  domnmsuppn0  49686  rmsuppss  49687  scmsuppss  49688  rrx2linest  50059  itscnhlinecirc02p  50102  inlinecirc02plem  50103  aacllem  51219