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  4331  ssn0  4367  uniintsn  4949  funopsn  7120  dff14i  7234  f1prex  7259  poxp3  8129  ressuppssdif  8164  suppfnss  8168  suppssov1  8176  suppssov2  8177  suppssfv  8181  omord  8532  nnmord  8596  mapdom2  9112  kmlem9  10112  isf32lem7  10312  1re  11174  addrid  11354  addn0nid  11598  nn0n0n1ge2  12510  xnegdi  13208  fseqsupubi  13943  sqrtgt0  15224  supcvg  15822  ntrivcvgfvn0  15865  efne0d  16063  efne0OLD  16065  divgcdcoprmex  16636  pceulem  16816  pcqmul  16824  pcqcl  16827  pcaddlem  16859  pcadd  16860  grpinvnz  18942  symgfvne  19311  symg2bas  19323  odmulgeq  19487  gsumval3lem2  19836  gsumval3  19837  ring1ne0  20208  ringelnzr  20432  0ringnnzr  20434  abvdom  20739  lmodfopne  20806  mptscmfsupp0  20833  lmodindp1  20920  lspsneleq  21025  lspsneq  21032  lspexch  21039  lspindp3  21046  lspsnsubn0  21050  dsmmsubg  21652  dsmmlss  21653  elfrlmbasn0  21672  coe1tmmul2  22162  ply1scln0  22178  mavmulsolcl  22438  0ntr  22958  elcls3  22970  neindisj  23004  neindisj2  23010  conndisj  23303  dfconn2  23306  fbunfip  23756  deg1mul2  26019  ply1nzb  26028  ne0p  26112  dgreq0  26171  dgradd2  26174  dgrcolem2  26180  elqaalem3  26229  logcj  26515  argimgt0  26521  tanarg  26528  cxpsqrtth  26639  dvcnsqrt  26653  ang180lem2  26720  ftalem2  26984  ftalem4  26986  ftalem5  26987  dvdssqf  27048  scutbdaylt  27730  expsne0  28321  lmimid  28721  lmiisolem  28723  hypcgrlem1  28726  hypcgrlem2  28727  f1otrg  28798  f1otrge  28799  ax5seglem4  28859  ax5seglem5  28860  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  pthdivtx  29657  spthdep  29664  usgr2wlkneq  29686  usgr2trlncl  29690  clwwlkccat  29919  clwwlkwwlksb  29983  clwwlknonel  30024  3pthdlem1  30093  uhgr3cyclexlem  30110  frgrwopreglem4a  30239  frrusgrord0lem  30268  nmlno0lem  30722  hlipgt0  30843  h1dn0  31481  spansneleq  31499  h1datomi  31510  nmlnop0iALT  31924  superpos  32283  chirredi  32323  preimane  32594  preiman0  32633  ogrpaddlt  33031  psgnfzto1stlem  33057  cycpmrn  33100  rmfsupp2  33189  pidlnzb  33393  drngidlhash  33405  constrsqrtcl  33769  qqhval2lem  33971  derangenlem  35158  subfacp1lem5  35171  btwndiff  36015  btwnconn1lem7  36081  btwnconn1lem12  36086  tan2h  37606  poimirlem1  37615  poimirlem9  37623  poimirlem17  37631  poimirlem22  37636  areacirclem1  37702  isdrngo2  37952  isdrngo3  37953  lsatn0  38992  lsatspn0  38993  lkrlspeqN  39164  cvlsupr2  39336  dalem25  39692  4atexlemcnd  40066  ltrncnvnid  40121  trlator0  40165  ltrnnidn  40168  trlnid  40173  cdleme3b  40223  cdleme11l  40263  cdleme16b  40273  cdleme35h2  40451  cdleme38n  40458  cdlemg8c  40623  cdlemg11a  40631  cdlemg12e  40641  cdlemg18a  40672  trlcoat  40717  trlcone  40722  tendo1ne0  40822  cdleml9  40978  dvheveccl  41106  dihmeetlem13N  41313  dihlspsnat  41327  dihpN  41330  dihatexv  41332  dochsat  41377  dochkrshp  41380  dochkr1  41472  lcfrlem28  41564  lcfrlem32  41568  mapdn0  41663  mapdpglem11  41676  mapdpglem16  41681  sticksstones1  42134  sn-1ne2  42253  pell1234qrne0  42841  jm2.26lem3  42990  2zrngnmlid  48243  2zrngnmrid  48244  2zrngnmlid2  48245  domnmsuppn0  48357  rmsuppss  48358  scmsuppss  48359  rrx2linest  48731  itscnhlinecirc02p  48774  inlinecirc02plem  48775  aacllem  49790