Theorem necon3d 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  pssdifn0  4321  ssn0  4357  uniintsn  4938  funopsn  7086  dff14i  7200  f1prex  7225  poxp3  8090  ressuppssdif  8125  suppfnss  8129  suppssov1  8137  suppssov2  8138  suppssfv  8142  omord  8493  nnmord  8557  mapdom2  9072  kmlem9  10072  isf32lem7  10272  1re  11134  addrid  11314  addn0nid  11558  nn0n0n1ge2  12470  xnegdi  13168  fseqsupubi  13903  sqrtgt0  15183  supcvg  15781  ntrivcvgfvn0  15824  efne0d  16022  efne0OLD  16024  divgcdcoprmex  16595  pceulem  16775  pcqmul  16783  pcqcl  16786  pcaddlem  16818  pcadd  16819  grpinvnz  18907  symgfvne  19278  symg2bas  19290  odmulgeq  19454  gsumval3lem2  19803  gsumval3  19804  ogrpaddlt  20035  ring1ne0  20202  ringelnzr  20426  0ringnnzr  20428  abvdom  20733  lmodfopne  20821  mptscmfsupp0  20848  lmodindp1  20935  lspsneleq  21040  lspsneq  21047  lspexch  21054  lspindp3  21061  lspsnsubn0  21065  dsmmsubg  21668  dsmmlss  21669  elfrlmbasn0  21688  coe1tmmul2  22178  ply1scln0  22194  mavmulsolcl  22454  0ntr  22974  elcls3  22986  neindisj  23020  neindisj2  23026  conndisj  23319  dfconn2  23322  fbunfip  23772  deg1mul2  26035  ply1nzb  26044  ne0p  26128  dgreq0  26187  dgradd2  26190  dgrcolem2  26196  elqaalem3  26245  logcj  26531  argimgt0  26537  tanarg  26544  cxpsqrtth  26655  dvcnsqrt  26669  ang180lem2  26736  ftalem2  27000  ftalem4  27002  ftalem5  27003  dvdssqf  27064  scutbdaylt  27747  expsne0  28346  lmimid  28757  lmiisolem  28759  hypcgrlem1  28762  hypcgrlem2  28763  f1otrg  28834  f1otrge  28835  ax5seglem4  28895  ax5seglem5  28896  axeuclid  28926  axcontlem2  28928  axcontlem4  28930  pthdivtx  29690  spthdep  29697  usgr2wlkneq  29719  usgr2trlncl  29723  clwwlkccat  29952  clwwlkwwlksb  30016  clwwlknonel  30057  3pthdlem1  30126  uhgr3cyclexlem  30143  frgrwopreglem4a  30272  frrusgrord0lem  30301  nmlno0lem  30755  hlipgt0  30876  h1dn0  31514  spansneleq  31532  h1datomi  31543  nmlnop0iALT  31957  superpos  32316  chirredi  32356  preimane  32627  preiman0  32666  psgnfzto1stlem  33055  cycpmrn  33098  rmfsupp2  33188  pidlnzb  33369  drngidlhash  33381  constrsqrtcl  33745  qqhval2lem  33947  derangenlem  35143  subfacp1lem5  35156  btwndiff  36000  btwnconn1lem7  36066  btwnconn1lem12  36071  tan2h  37591  poimirlem1  37600  poimirlem9  37608  poimirlem17  37616  poimirlem22  37621  areacirclem1  37687  isdrngo2  37937  isdrngo3  37938  lsatn0  38977  lsatspn0  38978  lkrlspeqN  39149  cvlsupr2  39321  dalem25  39677  4atexlemcnd  40051  ltrncnvnid  40106  trlator0  40150  ltrnnidn  40153  trlnid  40158  cdleme3b  40208  cdleme11l  40248  cdleme16b  40258  cdleme35h2  40436  cdleme38n  40443  cdlemg8c  40608  cdlemg11a  40616  cdlemg12e  40626  cdlemg18a  40657  trlcoat  40702  trlcone  40707  tendo1ne0  40807  cdleml9  40963  dvheveccl  41091  dihmeetlem13N  41298  dihlspsnat  41312  dihpN  41315  dihatexv  41317  dochsat  41362  dochkrshp  41365  dochkr1  41457  lcfrlem28  41549  lcfrlem32  41553  mapdn0  41648  mapdpglem11  41661  mapdpglem16  41666  sticksstones1  42119  sn-1ne2  42238  pell1234qrne0  42826  jm2.26lem3  42974  2zrngnmlid  48240  2zrngnmrid  48241  2zrngnmlid2  48242  domnmsuppn0  48354  rmsuppss  48355  scmsuppss  48356  rrx2linest  48728  itscnhlinecirc02p  48771  inlinecirc02plem  48772  aacllem  49787