Theorem necon3d 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pssdifn0  4322  ssn0  4358  uniintsn  4942  funopsn  7103  dff14i  7215  f1prex  7240  poxp3  8102  ressuppssdif  8137  suppfnss  8141  suppssov1  8149  suppssov2  8150  suppssfv  8154  omord  8505  nnmord  8570  mapdom2  9088  kmlem9  10081  isf32lem7  10281  1re  11144  addrid  11325  addn0nid  11569  nn0n0n1ge2  12481  xnegdi  13175  fseqsupubi  13913  sqrtgt0  15193  supcvg  15791  ntrivcvgfvn0  15834  efne0d  16032  efne0OLD  16034  divgcdcoprmex  16605  pceulem  16785  pcqmul  16793  pcqcl  16796  pcaddlem  16828  pcadd  16829  grpinvnz  18952  symgfvne  19322  symg2bas  19334  odmulgeq  19498  gsumval3lem2  19847  gsumval3  19848  ogrpaddlt  20079  ring1ne0  20246  ringelnzr  20468  0ringnnzr  20470  abvdom  20775  lmodfopne  20863  mptscmfsupp0  20890  lmodindp1  20977  lspsneleq  21082  lspsneq  21089  lspexch  21096  lspindp3  21103  lspsnsubn0  21107  dsmmsubg  21710  dsmmlss  21711  elfrlmbasn0  21730  coe1tmmul2  22230  ply1scln0  22246  mavmulsolcl  22507  0ntr  23027  elcls3  23039  neindisj  23073  neindisj2  23079  conndisj  23372  dfconn2  23375  fbunfip  23825  deg1mul2  26087  ply1nzb  26096  ne0p  26180  dgreq0  26239  dgradd2  26242  dgrcolem2  26248  elqaalem3  26297  logcj  26583  argimgt0  26589  tanarg  26596  cxpsqrtth  26707  dvcnsqrt  26721  ang180lem2  26788  ftalem2  27052  ftalem4  27054  ftalem5  27055  dvdssqf  27116  cutbdaylt  27806  expsne0  28444  lmimid  28878  lmiisolem  28880  hypcgrlem1  28883  hypcgrlem2  28884  f1otrg  28955  f1otrge  28956  ax5seglem4  29017  ax5seglem5  29018  axeuclid  29048  axcontlem2  29050  axcontlem4  29052  pthdivtx  29812  spthdep  29819  usgr2wlkneq  29841  usgr2trlncl  29845  clwwlkccat  30077  clwwlkwwlksb  30141  clwwlknonel  30182  3pthdlem1  30251  uhgr3cyclexlem  30268  frgrwopreglem4a  30397  frrusgrord0lem  30426  nmlno0lem  30880  hlipgt0  31001  h1dn0  31639  spansneleq  31657  h1datomi  31668  nmlnop0iALT  32082  superpos  32441  chirredi  32481  preimane  32758  preiman0  32799  psgnfzto1stlem  33193  cycpmrn  33236  rmfsupp2  33331  pidlnzb  33514  drngidlhash  33526  extdgfialglem2  33870  constrsqrtcl  33956  qqhval2lem  34158  derangenlem  35384  subfacp1lem5  35397  btwndiff  36240  btwnconn1lem7  36306  btwnconn1lem12  36311  tan2h  37857  poimirlem1  37866  poimirlem9  37874  poimirlem17  37882  poimirlem22  37887  areacirclem1  37953  isdrngo2  38203  isdrngo3  38204  lsatn0  39369  lsatspn0  39370  lkrlspeqN  39541  cvlsupr2  39713  dalem25  40068  4atexlemcnd  40442  ltrncnvnid  40497  trlator0  40541  ltrnnidn  40544  trlnid  40549  cdleme3b  40599  cdleme11l  40639  cdleme16b  40649  cdleme35h2  40827  cdleme38n  40834  cdlemg8c  40999  cdlemg11a  41007  cdlemg12e  41017  cdlemg18a  41048  trlcoat  41093  trlcone  41098  tendo1ne0  41198  cdleml9  41354  dvheveccl  41482  dihmeetlem13N  41689  dihlspsnat  41703  dihpN  41706  dihatexv  41708  dochsat  41753  dochkrshp  41756  dochkr1  41848  lcfrlem28  41940  lcfrlem32  41944  mapdn0  42039  mapdpglem11  42052  mapdpglem16  42057  sticksstones1  42510  sn-1ne2  42629  pell1234qrne0  43204  jm2.26lem3  43352  2zrngnmlid  48609  2zrngnmrid  48610  2zrngnmlid2  48611  domnmsuppn0  48723  rmsuppss  48724  scmsuppss  48725  rrx2linest  49096  itscnhlinecirc02p  49139  inlinecirc02plem  49140  aacllem  50154