Theorem necon3d 2981

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 2973	. 2 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵))
3		df-ne 2961	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 255	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  pssdifn0  4324  ssn0  4361  uniintsn  4946  funopsnOLD  7135  dff14i  7247  f1prex  7272  poxp3  8134  ressuppssdif  8169  suppfnss  8173  suppssov1  8181  suppssov2  8182  suppssfv  8186  omord  8541  nnmord  8606  mapdom2  9124  kmlem9  10130  isf32lem7  10331  1re  11196  addrid  11378  addn0nid  11622  nn0n0n1ge2  12563  xnegdi  13265  fseqsupubi  14005  sqrtgt0  15299  supcvg  15900  ntrivcvgfvn0  15943  efne0d  16141  efne0OLD  16143  divgcdcoprmex  16714  pceulem  16895  pcqmul  16903  pcqcl  16906  pcaddlem  16938  pcadd  16939  grpinvnz  19067  symgfvne  19442  symg2bas  19454  odmulgeq  19618  gsumval3lem2  19967  gsumval3  19968  ogrpaddlt  20199  ring1ne0  20373  ringelnzr  20598  0ringnnzr  20600  abvdom  20902  lmodfopne  20990  mptscmfsupp0  21017  lmodindp1  21104  lspsneleq  21208  lspsneq  21215  lspexch  21222  lspindp3  21229  lspsnsubn0  21233  dsmmsubg  21853  dsmmlss  21854  elfrlmbasn0  21873  coe1tmmul2  22397  ply1scln0  22412  mavmulsolcl  22669  0ntr  23189  elcls3  23201  neindisj  23235  neindisj2  23241  conndisj  23534  dfconn2  23537  fbunfip  23987  deg1mul2  26232  ply1nzb  26241  ne0p  26325  dgreq0  26383  dgradd2  26386  dgrcolem2  26392  elqaalem3  26443  logcj  26729  argimgt0  26735  tanarg  26742  cxpsqrtth  26853  dvcnsqrt  26867  ang180lem2  26933  ftalem2  27196  ftalem4  27198  ftalem5  27199  dvdssqf  27260  cutbdaylt  27949  expsne0  28587  lmimid  29046  lmiisolem  29048  hypcgrlem1  29051  hypcgrlem2  29052  f1otrg  29129  f1otrge  29130  ax5seglem4  29191  ax5seglem5  29192  axeuclid  29222  axcontlem2  29224  axcontlem4  29226  pthdivtx  29985  spthdep  29992  usgr2wlkneq  30014  usgr2trlncl  30018  clwwlkccat  30250  clwwlkwwlksb  30314  clwwlknonel  30355  3pthdlem1  30424  uhgr3cyclexlem  30441  frgrwopreglem4a  30570  frrusgrord0lem  30599  nmlno0lem  31054  hlipgt0  31175  h1dn0  31813  spansneleq  31831  h1datomi  31842  nmlnop0iALT  32256  superpos  32615  chirredi  32655  preimane  32926  preiman0  32967  psgnfzto1stlem  33333  cycpmrn  33376  rmfsupp2  33470  pidlnzb  33646  drngidlhash  33658  extdgfialglem2  34000  constrsqrtcl  34086  qqhval2lem  34288  derangenlem  35534  subfacp1lem5  35547  btwndiff  36390  btwnconn1lem7  36456  btwnconn1lem12  36461  mh-inf3f1  36914  tan2h  38123  poimirlem1  38132  poimirlem9  38140  poimirlem17  38148  poimirlem22  38153  areacirclem1  38219  isdrngo2  38469  isdrngo3  38470  lsatn0  39635  lsatspn0  39636  lkrlspeqN  39807  cvlsupr2  39979  dalem25  40334  4atexlemcnd  40708  ltrncnvnid  40763  trlator0  40807  ltrnnidn  40810  trlnid  40815  cdleme3b  40865  cdleme11l  40905  cdleme16b  40915  cdleme35h2  41093  cdleme38n  41100  cdlemg8c  41265  cdlemg11a  41273  cdlemg12e  41283  cdlemg18a  41314  trlcoat  41359  trlcone  41364  tendo1ne0  41464  cdleml9  41620  dvheveccl  41748  dihmeetlem13N  41955  dihlspsnat  41969  dihpN  41972  dihatexv  41974  dochsat  42019  dochkrshp  42022  dochkr1  42114  lcfrlem28  42206  lcfrlem32  42210  mapdn0  42305  mapdpglem11  42318  mapdpglem16  42323  sticksstones1  42775  sn-1ne2  42892  pell1234qrne0  43442  jm2.26lem3  43590  2zrngnmlid  48875  2zrngnmrid  48876  2zrngnmlid2  48877  domnmsuppn0  49000  rmsuppss  49001  scmsuppss  49002  rrx2linest  49373  itscnhlinecirc02p  49416  inlinecirc02plem  49417  aacllem  50430