Theorem necon3d 2978

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

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

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 2958

This theorem is used by:  pssdifn0  4319  ssn0  4358  uniintsn  4948  funopsnOLD  7149  dff14i  7260  f1prex  7289  poxp3  8152  ressuppssdif  8187  suppfnss  8191  suppssov1  8199  suppssov2  8200  suppssfv  8204  omord  8559  nnmord  8624  mapdom2  9150  kmlem9  10165  isf32lem7  10365  1re  11236  addrid  11418  addn0nid  11662  nn0n0n1ge2  12600  xnegdi  13304  fseqsupubi  14046  sqrtgt0  15349  supcvg  15949  ntrivcvgfvn0  15992  efne0d  16189  efne0OLD  16191  divgcdcoprmex  16762  pceulem  16943  pcqmul  16951  pcqcl  16954  pcaddlem  16986  pcadd  16987  grpinvnz  19139  symgfvne  19514  symg2bas  19526  odmulgeq  19690  gsumval3lem2  20039  gsumval3  20040  ogrpaddlt  20271  ring1ne0  20447  ringelnzr  20690  0ringnnzr  20692  isdrng3lem2  20921  isdrng5  20923  abvdom  21002  lmodfopne  21090  mptscmfsupp0  21117  lmodindp1  21204  lspsneleq  21308  lspsneq  21315  lspexch  21322  lspindp3  21329  lspsnsubn0  21333  dsmmsubg  21962  dsmmlss  21963  elfrlmbasn0  21982  coe1tmmul2  22508  ply1scln0  22523  mavmulsolcl  22779  0ntr  23302  elcls3  23314  neindisj  23348  neindisj2  23354  conndisj  23647  dfconn2  23650  fbunfip  24101  deg1mul2  26346  ply1nzb  26355  ne0p  26439  dgreq0  26498  dgradd2  26501  dgrcolem2  26507  elqaalem3  26560  logcj  26851  argimgt0  26857  tanarg  26864  cxpsqrtth  26975  dvcnsqrt  26989  ang180lem2  27055  ftalem2  27318  ftalem4  27320  ftalem5  27321  dvdssqf  27382  cutbdaylt  28071  expsne0  28709  lmimid  29186  lmiisolem  29188  hypcgrlem1  29192  hypcgrlem2  29193  f1otrg  29335  f1otrge  29336  ax5seglem4  29397  ax5seglem5  29398  axeuclid  29428  axcontlem2  29430  axcontlem4  29432  pthdivtx  30199  spthdep  30207  usgr2wlkneq  30229  usgr2trlncl  30233  clwwlkccat  30468  clwwlkwwlksb  30532  clwwlknonel  30573  3pthdlem1  30652  uhgr3cyclexlem  30669  frgrwopreglem4a  30798  frrusgrord0lem  30827  nmlno0lem  31282  hlipgt0  31403  h1dn0  32041  spansneleq  32059  h1datomi  32070  nmlnop0iALT  32484  superpos  32843  chirredi  32883  preimane  33150  preiman0  33190  psgnfzto1stlem  33548  cycpmrn  33591  rmfsupp2  33685  pidlnzb  33858  drngidlhash  33869  extdgfialglem2  34211  constrsqrtcl  34297  qqhval2lem  34499  derangenlem  35758  subfacp1lem5  35771  btwndiff  36615  btwnconn1lem7  36681  btwnconn1lem12  36686  mh-inf3f1  37168  tan2h  38374  poimirlem1  38378  poimirlem9  38386  poimirlem17  38394  poimirlem22  38399  areacirclem1  38465  isdrngo2  38716  isdrngo3  38717  lsatn0  39880  lsatspn0  39881  lkrlspeqN  40052  cvlsupr2  40224  dalem25  40579  4atexlemcnd  40953  ltrncnvnid  41008  trlator0  41052  ltrnnidn  41055  trlnid  41060  cdleme3b  41110  cdleme11l  41150  cdleme16b  41160  cdleme35h2  41338  cdleme38n  41345  cdlemg8c  41510  cdlemg11a  41518  cdlemg12e  41528  cdlemg18a  41559  trlcoat  41604  trlcone  41609  tendo1ne0  41709  cdleml9  41865  dvheveccl  41993  dihmeetlem13N  42200  dihlspsnat  42214  dihpN  42217  dihatexv  42219  dochsat  42264  dochkrshp  42267  dochkr1  42359  lcfrlem28  42451  lcfrlem32  42455  mapdn0  42550  mapdpglem11  42563  mapdpglem16  42568  sticksstones1  43020  sn-1ne2  43154  pell1234qrne0  43702  jm2.26lem3  43850  2zrngnmlid  49178  2zrngnmrid  49179  2zrngnmlid2  49180  domnmsuppn0  49307  rmsuppss  49308  scmsuppss  49309  rrx2linest  49680  itscnhlinecirc02p  49723  inlinecirc02plem  49724  aacllem  50780