Theorem necon3d 2950

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

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

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 2930

This theorem is referenced by:  pssdifn0  4317  ssn0  4353  uniintsn  4935  funopsn  7087  dff14i  7199  f1prex  7224  poxp3  8086  ressuppssdif  8121  suppfnss  8125  suppssov1  8133  suppssov2  8134  suppssfv  8138  omord  8489  nnmord  8553  mapdom2  9068  kmlem9  10057  isf32lem7  10257  1re  11119  addrid  11300  addn0nid  11544  nn0n0n1ge2  12456  xnegdi  13149  fseqsupubi  13887  sqrtgt0  15167  supcvg  15765  ntrivcvgfvn0  15808  efne0d  16006  efne0OLD  16008  divgcdcoprmex  16579  pceulem  16759  pcqmul  16767  pcqcl  16770  pcaddlem  16802  pcadd  16803  grpinvnz  18925  symgfvne  19295  symg2bas  19307  odmulgeq  19471  gsumval3lem2  19820  gsumval3  19821  ogrpaddlt  20052  ring1ne0  20219  ringelnzr  20440  0ringnnzr  20442  abvdom  20747  lmodfopne  20835  mptscmfsupp0  20862  lmodindp1  20949  lspsneleq  21054  lspsneq  21061  lspexch  21068  lspindp3  21075  lspsnsubn0  21079  dsmmsubg  21682  dsmmlss  21683  elfrlmbasn0  21702  coe1tmmul2  22191  ply1scln0  22207  mavmulsolcl  22467  0ntr  22987  elcls3  22999  neindisj  23033  neindisj2  23039  conndisj  23332  dfconn2  23335  fbunfip  23785  deg1mul2  26047  ply1nzb  26056  ne0p  26140  dgreq0  26199  dgradd2  26202  dgrcolem2  26208  elqaalem3  26257  logcj  26543  argimgt0  26549  tanarg  26556  cxpsqrtth  26667  dvcnsqrt  26681  ang180lem2  26748  ftalem2  27012  ftalem4  27014  ftalem5  27015  dvdssqf  27076  scutbdaylt  27760  expsne0  28360  lmimid  28773  lmiisolem  28775  hypcgrlem1  28778  hypcgrlem2  28779  f1otrg  28850  f1otrge  28851  ax5seglem4  28912  ax5seglem5  28913  axeuclid  28943  axcontlem2  28945  axcontlem4  28947  pthdivtx  29707  spthdep  29714  usgr2wlkneq  29736  usgr2trlncl  29740  clwwlkccat  29972  clwwlkwwlksb  30036  clwwlknonel  30077  3pthdlem1  30146  uhgr3cyclexlem  30163  frgrwopreglem4a  30292  frrusgrord0lem  30321  nmlno0lem  30775  hlipgt0  30896  h1dn0  31534  spansneleq  31552  h1datomi  31563  nmlnop0iALT  31977  superpos  32336  chirredi  32376  preimane  32654  preiman0  32695  psgnfzto1stlem  33076  cycpmrn  33119  rmfsupp2  33212  pidlnzb  33394  drngidlhash  33406  extdgfialglem2  33727  constrsqrtcl  33813  qqhval2lem  34015  derangenlem  35236  subfacp1lem5  35249  btwndiff  36092  btwnconn1lem7  36158  btwnconn1lem12  36163  tan2h  37672  poimirlem1  37681  poimirlem9  37689  poimirlem17  37697  poimirlem22  37702  areacirclem1  37768  isdrngo2  38018  isdrngo3  38019  lsatn0  39118  lsatspn0  39119  lkrlspeqN  39290  cvlsupr2  39462  dalem25  39817  4atexlemcnd  40191  ltrncnvnid  40246  trlator0  40290  ltrnnidn  40293  trlnid  40298  cdleme3b  40348  cdleme11l  40388  cdleme16b  40398  cdleme35h2  40576  cdleme38n  40583  cdlemg8c  40748  cdlemg11a  40756  cdlemg12e  40766  cdlemg18a  40797  trlcoat  40842  trlcone  40847  tendo1ne0  40947  cdleml9  41103  dvheveccl  41231  dihmeetlem13N  41438  dihlspsnat  41452  dihpN  41455  dihatexv  41457  dochsat  41502  dochkrshp  41505  dochkr1  41597  lcfrlem28  41689  lcfrlem32  41693  mapdn0  41788  mapdpglem11  41801  mapdpglem16  41806  sticksstones1  42259  sn-1ne2  42383  pell1234qrne0  42970  jm2.26lem3  43118  2zrngnmlid  48379  2zrngnmrid  48380  2zrngnmlid2  48381  domnmsuppn0  48493  rmsuppss  48494  scmsuppss  48495  rrx2linest  48867  itscnhlinecirc02p  48910  inlinecirc02plem  48911  aacllem  49926