Theorem necon3d 2977

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

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

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 2957

This theorem is used by:  pssdifn0  4316  ssn0  4355  uniintsn  4945  funopsnOLD  7152  dff14i  7263  f1prex  7292  poxp3  8167  ressuppssdif  8202  suppfnss  8206  suppssov1  8214  suppssov2  8215  suppssfv  8219  omord  8576  nnmord  8641  mapdom2  9167  kmlem9  10237  isf32lem7  10437  1re  11308  addrid  11490  addn0nid  11736  nn0n0n1ge2  12674  xnegdi  13378  fseqsupubi  14121  sqrtgt0  15425  supcvg  16025  ntrivcvgfvn0  16068  efne0d  16263  efne0OLD  16265  divgcdcoprmex  16841  pceulem  17023  pcqmul  17031  pcqcl  17034  pcaddlem  17066  pcadd  17067  grpinvnz  19220  symgfvne  19595  symg2bas  19607  odmulgeq  19771  gsumval3lem2  20120  gsumval3  20121  ogrpaddlt  20352  ring1ne0  20530  ringelnzr  20774  0ringnnzr  20776  isdrng3lem2  21006  isdrng5  21008  abvdom  21087  lmodfopne  21175  mptscmfsupp0  21202  lmodindp1  21289  lspsneleq  21393  lspsneq  21400  lspexch  21407  lspindp3  21414  lspsnsubn0  21418  dsmmsubg  22049  dsmmlss  22050  elfrlmbasn0  22069  coe1tmmul2  22595  ply1scln0  22610  mavmulsolcl  22866  0ntr  23389  elcls3  23401  neindisj  23435  neindisj2  23441  conndisj  23734  dfconn2  23737  fbunfip  24188  deg1mul2  26432  ply1nzb  26441  ne0p  26525  dgreq0  26584  dgradd2  26587  dgrcolem2  26593  elqaalem3  26644  logcj  26934  argimgt0  26940  tanarg  26947  cxpsqrtth  27058  dvcnsqrt  27072  ang180lem2  27138  ftalem2  27401  ftalem4  27403  ftalem5  27404  dvdssqf  27465  cutbdaylt  28184  expsne0  28822  lmimid  29299  lmiisolem  29301  hypcgrlem1  29305  hypcgrlem2  29306  f1otrg  29448  f1otrge  29449  ax5seglem4  29510  ax5seglem5  29511  axeuclid  29541  axcontlem2  29543  axcontlem4  29545  pthdivtx  30312  spthdep  30320  usgr2wlkneq  30342  usgr2trlncl  30346  clwwlkccat  30581  clwwlkwwlksb  30645  clwwlknonel  30686  3pthdlem1  30765  uhgr3cyclexlem  30782  frgrwopreglem4a  30911  frrusgrord0lem  30940  nmlno0lem  31395  hlipgt0  31516  h1dn0  32154  spansneleq  32172  h1datomi  32183  nmlnop0iALT  32597  superpos  32956  chirredi  32996  preimane  33263  preiman0  33303  psgnfzto1stlem  33661  cycpmrn  33704  rmfsupp2  33798  pidlnzb  33972  drngidlhash  33983  extdgfialglem2  34325  constrsqrtcl  34411  qqhval2lem  34613  derangenlem  35936  subfacp1lem5  35949  btwndiff  36792  btwnconn1lem7  36858  btwnconn1lem12  36863  tan2h  38535  poimirlem1  38539  poimirlem9  38547  poimirlem17  38555  poimirlem22  38560  areacirclem1  38626  isdrngo2  38892  isdrngo3  38893  lsatn0  40056  lsatspn0  40057  lkrlspeqN  40228  cvlsupr2  40400  dalem25  40755  4atexlemcnd  41129  ltrncnvnid  41184  trlator0  41228  ltrnnidn  41231  trlnid  41236  cdleme3b  41286  cdleme11l  41326  cdleme16b  41336  cdleme35h2  41514  cdleme38n  41521  cdlemg8c  41686  cdlemg11a  41694  cdlemg12e  41704  cdlemg18a  41735  trlcoat  41780  trlcone  41785  tendo1ne0  41885  cdleml9  42041  dvheveccl  42169  dihmeetlem13N  42376  dihlspsnat  42390  dihpN  42393  dihatexv  42395  dochsat  42440  dochkrshp  42443  dochkr1  42535  lcfrlem28  42627  lcfrlem32  42631  mapdn0  42726  mapdpglem11  42739  mapdpglem16  42744  sticksstones1  43196  sn-1ne2  43330  pell1234qrne0  43859  jm2.26lem3  44007  2zrngnmlid  49351  2zrngnmrid  49352  2zrngnmlid2  49353  domnmsuppn0  49480  rmsuppss  49481  scmsuppss  49482  rrx2linest  49853  itscnhlinecirc02p  49896  inlinecirc02plem  49897  aacllem  50938