Theorem necon3d 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  pssdifn0  4320  ssn0  4356  uniintsn  4940  funopsn  7093  dff14i  7205  f1prex  7230  poxp3  8092  ressuppssdif  8127  suppfnss  8131  suppssov1  8139  suppssov2  8140  suppssfv  8144  omord  8495  nnmord  8560  mapdom2  9076  kmlem9  10069  isf32lem7  10269  1re  11132  addrid  11313  addn0nid  11557  nn0n0n1ge2  12469  xnegdi  13163  fseqsupubi  13901  sqrtgt0  15181  supcvg  15779  ntrivcvgfvn0  15822  efne0d  16020  efne0OLD  16022  divgcdcoprmex  16593  pceulem  16773  pcqmul  16781  pcqcl  16784  pcaddlem  16816  pcadd  16817  grpinvnz  18940  symgfvne  19310  symg2bas  19322  odmulgeq  19486  gsumval3lem2  19835  gsumval3  19836  ogrpaddlt  20067  ring1ne0  20234  ringelnzr  20456  0ringnnzr  20458  abvdom  20763  lmodfopne  20851  mptscmfsupp0  20878  lmodindp1  20965  lspsneleq  21070  lspsneq  21077  lspexch  21084  lspindp3  21091  lspsnsubn0  21095  dsmmsubg  21698  dsmmlss  21699  elfrlmbasn0  21718  coe1tmmul2  22218  ply1scln0  22234  mavmulsolcl  22495  0ntr  23015  elcls3  23027  neindisj  23061  neindisj2  23067  conndisj  23360  dfconn2  23363  fbunfip  23813  deg1mul2  26075  ply1nzb  26084  ne0p  26168  dgreq0  26227  dgradd2  26230  dgrcolem2  26236  elqaalem3  26285  logcj  26571  argimgt0  26577  tanarg  26584  cxpsqrtth  26695  dvcnsqrt  26709  ang180lem2  26776  ftalem2  27040  ftalem4  27042  ftalem5  27043  dvdssqf  27104  cutbdaylt  27794  expsne0  28432  lmimid  28866  lmiisolem  28868  hypcgrlem1  28871  hypcgrlem2  28872  f1otrg  28943  f1otrge  28944  ax5seglem4  29005  ax5seglem5  29006  axeuclid  29036  axcontlem2  29038  axcontlem4  29040  pthdivtx  29800  spthdep  29807  usgr2wlkneq  29829  usgr2trlncl  29833  clwwlkccat  30065  clwwlkwwlksb  30129  clwwlknonel  30170  3pthdlem1  30239  uhgr3cyclexlem  30256  frgrwopreglem4a  30385  frrusgrord0lem  30414  nmlno0lem  30868  hlipgt0  30989  h1dn0  31627  spansneleq  31645  h1datomi  31656  nmlnop0iALT  32070  superpos  32429  chirredi  32469  preimane  32748  preiman0  32789  psgnfzto1stlem  33182  cycpmrn  33225  rmfsupp2  33320  pidlnzb  33503  drngidlhash  33515  extdgfialglem2  33850  constrsqrtcl  33936  qqhval2lem  34138  derangenlem  35365  subfacp1lem5  35378  btwndiff  36221  btwnconn1lem7  36287  btwnconn1lem12  36292  tan2h  37809  poimirlem1  37818  poimirlem9  37826  poimirlem17  37834  poimirlem22  37839  areacirclem1  37905  isdrngo2  38155  isdrngo3  38156  lsatn0  39255  lsatspn0  39256  lkrlspeqN  39427  cvlsupr2  39599  dalem25  39954  4atexlemcnd  40328  ltrncnvnid  40383  trlator0  40427  ltrnnidn  40430  trlnid  40435  cdleme3b  40485  cdleme11l  40525  cdleme16b  40535  cdleme35h2  40713  cdleme38n  40720  cdlemg8c  40885  cdlemg11a  40893  cdlemg12e  40903  cdlemg18a  40934  trlcoat  40979  trlcone  40984  tendo1ne0  41084  cdleml9  41240  dvheveccl  41368  dihmeetlem13N  41575  dihlspsnat  41589  dihpN  41592  dihatexv  41594  dochsat  41639  dochkrshp  41642  dochkr1  41734  lcfrlem28  41826  lcfrlem32  41830  mapdn0  41925  mapdpglem11  41938  mapdpglem16  41943  sticksstones1  42396  sn-1ne2  42516  pell1234qrne0  43091  jm2.26lem3  43239  2zrngnmlid  48497  2zrngnmrid  48498  2zrngnmlid2  48499  domnmsuppn0  48611  rmsuppss  48612  scmsuppss  48613  rrx2linest  48984  itscnhlinecirc02p  49027  inlinecirc02plem  49028  aacllem  50042