Theorem necon3d 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  pssdifn0  4373  ssn0  4409  uniintsn  4989  funopsn  7167  f1prex  7303  poxp3  8173  ressuppssdif  8208  suppfnss  8212  suppssov1  8220  suppssov2  8221  suppssfv  8225  omord  8604  nnmord  8668  mapdom2  9186  kmlem9  10196  isf32lem7  10396  1re  11258  addrid  11438  addn0nid  11680  nn0n0n1ge2  12591  xnegdi  13286  fseqsupubi  14015  sqrtgt0  15293  supcvg  15888  ntrivcvgfvn0  15931  efne0  16129  divgcdcoprmex  16699  pceulem  16878  pcqmul  16886  pcqcl  16889  pcaddlem  16921  pcadd  16922  grpinvnz  19040  symgfvne  19412  symg2bas  19424  odmulgeq  19589  gsumval3lem2  19938  gsumval3  19939  ring1ne0  20312  ringelnzr  20539  0ringnnzr  20541  abvdom  20847  lmodfopne  20914  mptscmfsupp0  20941  lmodindp1  21029  lspsneleq  21134  lspsneq  21141  lspexch  21148  lspindp3  21155  lspsnsubn0  21159  dsmmsubg  21780  dsmmlss  21781  elfrlmbasn0  21800  coe1tmmul2  22294  ply1scln0  22310  mavmulsolcl  22572  0ntr  23094  elcls3  23106  neindisj  23140  neindisj2  23146  conndisj  23439  dfconn2  23442  fbunfip  23892  deg1mul2  26167  ply1nzb  26176  ne0p  26260  dgreq0  26319  dgradd2  26322  dgrcolem2  26328  elqaalem3  26377  logcj  26662  argimgt0  26668  tanarg  26675  cxpsqrtth  26786  dvcnsqrt  26800  ang180lem2  26867  ftalem2  27131  ftalem4  27133  ftalem5  27134  dvdssqf  27195  scutbdaylt  27877  expsne0  28428  lmimid  28816  lmiisolem  28818  hypcgrlem1  28821  hypcgrlem2  28822  f1otrg  28893  f1otrge  28894  ax5seglem4  28961  ax5seglem5  28962  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  pthdivtx  29761  spthdep  29766  usgr2wlkneq  29788  usgr2trlncl  29792  clwwlkccat  30018  clwwlkwwlksb  30082  clwwlknonel  30123  3pthdlem1  30192  uhgr3cyclexlem  30209  frgrwopreglem4a  30338  frrusgrord0lem  30367  nmlno0lem  30821  hlipgt0  30942  h1dn0  31580  spansneleq  31598  h1datomi  31609  nmlnop0iALT  32023  superpos  32382  chirredi  32422  preimane  32686  preiman0  32724  ogrpaddlt  33076  psgnfzto1stlem  33102  cycpmrn  33145  rmfsupp2  33227  pidlnzb  33429  drngidlhash  33441  qqhval2lem  33943  derangenlem  35155  subfacp1lem5  35168  btwndiff  36008  btwnconn1lem7  36074  btwnconn1lem12  36079  tan2h  37598  poimirlem1  37607  poimirlem9  37615  poimirlem17  37623  poimirlem22  37628  areacirclem1  37694  isdrngo2  37944  isdrngo3  37945  lsatn0  38980  lsatspn0  38981  lkrlspeqN  39152  cvlsupr2  39324  dalem25  39680  4atexlemcnd  40054  ltrncnvnid  40109  trlator0  40153  ltrnnidn  40156  trlnid  40161  cdleme3b  40211  cdleme11l  40251  cdleme16b  40261  cdleme35h2  40439  cdleme38n  40446  cdlemg8c  40611  cdlemg11a  40619  cdlemg12e  40629  cdlemg18a  40660  trlcoat  40705  trlcone  40710  tendo1ne0  40810  cdleml9  40966  dvheveccl  41094  dihmeetlem13N  41301  dihlspsnat  41315  dihpN  41318  dihatexv  41320  dochsat  41365  dochkrshp  41368  dochkr1  41460  lcfrlem28  41552  lcfrlem32  41556  mapdn0  41651  mapdpglem11  41664  mapdpglem16  41669  sticksstones1  42127  sn-1ne2  42278  efne0d  42351  pell1234qrne0  42840  jm2.26lem3  42989  2zrngnmlid  48098  2zrngnmrid  48099  2zrngnmlid2  48100  domnmsuppn0  48213  rmsuppss  48214  scmsuppss  48215  rrx2linest  48591  itscnhlinecirc02p  48634  inlinecirc02plem  48635  aacllem  49031