Theorem necon3d 2979

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  pssdifn0  4324  ssn0  4363  uniintsn  4951  funopsnOLD  7147  dff14i  7259  f1prex  7284  poxp3  8147  ressuppssdif  8182  suppfnss  8186  suppssov1  8194  suppssov2  8195  suppssfv  8199  omord  8554  nnmord  8619  mapdom2  9137  kmlem9  10143  isf32lem7  10344  1re  11209  addrid  11391  addn0nid  11635  nn0n0n1ge2  12573  xnegdi  13275  fseqsupubi  14016  sqrtgt0  15311  supcvg  15912  ntrivcvgfvn0  15955  efne0d  16152  efne0OLD  16154  divgcdcoprmex  16725  pceulem  16906  pcqmul  16914  pcqcl  16917  pcaddlem  16949  pcadd  16950  grpinvnz  19077  symgfvne  19452  symg2bas  19464  odmulgeq  19628  gsumval3lem2  19977  gsumval3  19978  ogrpaddlt  20209  ring1ne0  20383  ringelnzr  20608  0ringnnzr  20610  abvdom  20914  lmodfopne  21002  mptscmfsupp0  21029  lmodindp1  21116  lspsneleq  21220  lspsneq  21227  lspexch  21234  lspindp3  21241  lspsnsubn0  21245  dsmmsubg  21874  dsmmlss  21875  elfrlmbasn0  21894  coe1tmmul2  22418  ply1scln0  22433  mavmulsolcl  22689  0ntr  23209  elcls3  23221  neindisj  23255  neindisj2  23261  conndisj  23554  dfconn2  23557  fbunfip  24007  deg1mul2  26252  ply1nzb  26261  ne0p  26345  dgreq0  26403  dgradd2  26406  dgrcolem2  26412  elqaalem3  26463  logcj  26749  argimgt0  26755  tanarg  26762  cxpsqrtth  26873  dvcnsqrt  26887  ang180lem2  26953  ftalem2  27216  ftalem4  27218  ftalem5  27219  dvdssqf  27280  cutbdaylt  27969  expsne0  28607  lmimid  29081  lmiisolem  29083  hypcgrlem1  29087  hypcgrlem2  29088  f1otrg  29198  f1otrge  29199  ax5seglem4  29260  ax5seglem5  29261  axeuclid  29291  axcontlem2  29293  axcontlem4  29295  pthdivtx  30054  spthdep  30061  usgr2wlkneq  30083  usgr2trlncl  30087  clwwlkccat  30319  clwwlkwwlksb  30383  clwwlknonel  30424  3pthdlem1  30493  uhgr3cyclexlem  30510  frgrwopreglem4a  30639  frrusgrord0lem  30668  nmlno0lem  31123  hlipgt0  31244  h1dn0  31882  spansneleq  31900  h1datomi  31911  nmlnop0iALT  32325  superpos  32684  chirredi  32724  preimane  32992  preiman0  33033  psgnfzto1stlem  33398  cycpmrn  33441  rmfsupp2  33535  pidlnzb  33708  drngidlhash  33719  extdgfialglem2  34061  constrsqrtcl  34147  qqhval2lem  34349  derangenlem  35641  subfacp1lem5  35654  btwndiff  36497  btwnconn1lem7  36563  btwnconn1lem12  36568  mh-inf3f1  37030  tan2h  38241  poimirlem1  38250  poimirlem9  38258  poimirlem17  38266  poimirlem22  38271  areacirclem1  38337  isdrngo2  38587  isdrngo3  38588  lsatn0  39751  lsatspn0  39752  lkrlspeqN  39923  cvlsupr2  40095  dalem25  40450  4atexlemcnd  40824  ltrncnvnid  40879  trlator0  40923  ltrnnidn  40926  trlnid  40931  cdleme3b  40981  cdleme11l  41021  cdleme16b  41031  cdleme35h2  41209  cdleme38n  41216  cdlemg8c  41381  cdlemg11a  41389  cdlemg12e  41399  cdlemg18a  41430  trlcoat  41475  trlcone  41480  tendo1ne0  41580  cdleml9  41736  dvheveccl  41864  dihmeetlem13N  42071  dihlspsnat  42085  dihpN  42088  dihatexv  42090  dochsat  42135  dochkrshp  42138  dochkr1  42230  lcfrlem28  42322  lcfrlem32  42326  mapdn0  42421  mapdpglem11  42434  mapdpglem16  42439  sticksstones1  42891  sn-1ne2  43010  pell1234qrne0  43560  jm2.26lem3  43708  2zrngnmlid  48997  2zrngnmrid  48998  2zrngnmlid2  48999  domnmsuppn0  49126  rmsuppss  49127  scmsuppss  49128  rrx2linest  49499  itscnhlinecirc02p  49542  inlinecirc02plem  49543  aacllem  50578