Theorem necon3d 2956

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  pssdifn0  4303  ssn0  4339  uniintsn  4922  funopsnOLD  7098  dff14i  7210  f1prex  7235  poxp3  8097  ressuppssdif  8132  suppfnss  8136  suppssov1  8144  suppssov2  8145  suppssfv  8149  omord  8500  nnmord  8565  mapdom2  9083  kmlem9  10079  isf32lem7  10279  1re  11142  addrid  11324  addn0nid  11568  nn0n0n1ge2  12503  xnegdi  13198  fseqsupubi  13938  sqrtgt0  15218  supcvg  15819  ntrivcvgfvn0  15862  efne0d  16060  efne0OLD  16062  divgcdcoprmex  16633  pceulem  16814  pcqmul  16822  pcqcl  16825  pcaddlem  16857  pcadd  16858  grpinvnz  18984  symgfvne  19354  symg2bas  19366  odmulgeq  19530  gsumval3lem2  19879  gsumval3  19880  ogrpaddlt  20111  ring1ne0  20278  ringelnzr  20502  0ringnnzr  20504  abvdom  20809  lmodfopne  20897  mptscmfsupp0  20924  lmodindp1  21011  lspsneleq  21115  lspsneq  21122  lspexch  21129  lspindp3  21136  lspsnsubn0  21140  dsmmsubg  21725  dsmmlss  21726  elfrlmbasn0  21745  coe1tmmul2  22269  ply1scln0  22284  mavmulsolcl  22541  0ntr  23061  elcls3  23073  neindisj  23107  neindisj2  23113  conndisj  23406  dfconn2  23409  fbunfip  23859  deg1mul2  26104  ply1nzb  26113  ne0p  26197  dgreq0  26255  dgradd2  26258  dgrcolem2  26264  elqaalem3  26312  logcj  26595  argimgt0  26601  tanarg  26608  cxpsqrtth  26719  dvcnsqrt  26733  ang180lem2  26799  ftalem2  27062  ftalem4  27064  ftalem5  27065  dvdssqf  27126  cutbdaylt  27815  expsne0  28453  lmimid  28887  lmiisolem  28889  hypcgrlem1  28892  hypcgrlem2  28893  f1otrg  28964  f1otrge  28965  ax5seglem4  29026  ax5seglem5  29027  axeuclid  29057  axcontlem2  29059  axcontlem4  29061  pthdivtx  29820  spthdep  29827  usgr2wlkneq  29849  usgr2trlncl  29853  clwwlkccat  30085  clwwlkwwlksb  30149  clwwlknonel  30190  3pthdlem1  30259  uhgr3cyclexlem  30276  frgrwopreglem4a  30405  frrusgrord0lem  30434  nmlno0lem  30889  hlipgt0  31010  h1dn0  31648  spansneleq  31666  h1datomi  31677  nmlnop0iALT  32091  superpos  32450  chirredi  32490  preimane  32768  preiman0  32809  psgnfzto1stlem  33188  cycpmrn  33231  rmfsupp2  33326  pidlnzb  33512  drngidlhash  33524  extdgfialglem2  33884  constrsqrtcl  33970  qqhval2lem  34172  derangenlem  35406  subfacp1lem5  35419  btwndiff  36262  btwnconn1lem7  36328  btwnconn1lem12  36333  mh-inf3f1  36776  tan2h  37986  poimirlem1  37995  poimirlem9  38003  poimirlem17  38011  poimirlem22  38016  areacirclem1  38082  isdrngo2  38332  isdrngo3  38333  lsatn0  39498  lsatspn0  39499  lkrlspeqN  39670  cvlsupr2  39842  dalem25  40197  4atexlemcnd  40571  ltrncnvnid  40626  trlator0  40670  ltrnnidn  40673  trlnid  40678  cdleme3b  40728  cdleme11l  40768  cdleme16b  40778  cdleme35h2  40956  cdleme38n  40963  cdlemg8c  41128  cdlemg11a  41136  cdlemg12e  41146  cdlemg18a  41177  trlcoat  41222  trlcone  41227  tendo1ne0  41327  cdleml9  41483  dvheveccl  41611  dihmeetlem13N  41818  dihlspsnat  41832  dihpN  41835  dihatexv  41837  dochsat  41882  dochkrshp  41885  dochkr1  41977  lcfrlem28  42069  lcfrlem32  42073  mapdn0  42168  mapdpglem11  42181  mapdpglem16  42186  sticksstones1  42638  sn-1ne2  42755  pell1234qrne0  43305  jm2.26lem3  43453  2zrngnmlid  48753  2zrngnmrid  48754  2zrngnmlid2  48755  domnmsuppn0  48867  rmsuppss  48868  scmsuppss  48869  rrx2linest  49240  itscnhlinecirc02p  49283  inlinecirc02plem  49284  aacllem  50298