Theorem necon3d 2949

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

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

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 2929

This theorem is referenced by:  pssdifn0  4318  ssn0  4354  uniintsn  4935  funopsn  7081  dff14i  7193  f1prex  7218  poxp3  8080  ressuppssdif  8115  suppfnss  8119  suppssov1  8127  suppssov2  8128  suppssfv  8132  omord  8483  nnmord  8547  mapdom2  9061  kmlem9  10047  isf32lem7  10247  1re  11109  addrid  11290  addn0nid  11534  nn0n0n1ge2  12446  xnegdi  13144  fseqsupubi  13882  sqrtgt0  15162  supcvg  15760  ntrivcvgfvn0  15803  efne0d  16001  efne0OLD  16003  divgcdcoprmex  16574  pceulem  16754  pcqmul  16762  pcqcl  16765  pcaddlem  16797  pcadd  16798  grpinvnz  18920  symgfvne  19291  symg2bas  19303  odmulgeq  19467  gsumval3lem2  19816  gsumval3  19817  ogrpaddlt  20048  ring1ne0  20215  ringelnzr  20436  0ringnnzr  20438  abvdom  20743  lmodfopne  20831  mptscmfsupp0  20858  lmodindp1  20945  lspsneleq  21050  lspsneq  21057  lspexch  21064  lspindp3  21071  lspsnsubn0  21075  dsmmsubg  21678  dsmmlss  21679  elfrlmbasn0  21698  coe1tmmul2  22188  ply1scln0  22204  mavmulsolcl  22464  0ntr  22984  elcls3  22996  neindisj  23030  neindisj2  23036  conndisj  23329  dfconn2  23332  fbunfip  23782  deg1mul2  26044  ply1nzb  26053  ne0p  26137  dgreq0  26196  dgradd2  26199  dgrcolem2  26205  elqaalem3  26254  logcj  26540  argimgt0  26546  tanarg  26553  cxpsqrtth  26664  dvcnsqrt  26678  ang180lem2  26745  ftalem2  27009  ftalem4  27011  ftalem5  27012  dvdssqf  27073  scutbdaylt  27757  expsne0  28357  lmimid  28770  lmiisolem  28772  hypcgrlem1  28775  hypcgrlem2  28776  f1otrg  28847  f1otrge  28848  ax5seglem4  28908  ax5seglem5  28909  axeuclid  28939  axcontlem2  28941  axcontlem4  28943  pthdivtx  29703  spthdep  29710  usgr2wlkneq  29732  usgr2trlncl  29736  clwwlkccat  29965  clwwlkwwlksb  30029  clwwlknonel  30070  3pthdlem1  30139  uhgr3cyclexlem  30156  frgrwopreglem4a  30285  frrusgrord0lem  30314  nmlno0lem  30768  hlipgt0  30889  h1dn0  31527  spansneleq  31545  h1datomi  31556  nmlnop0iALT  31970  superpos  32329  chirredi  32369  preimane  32647  preiman0  32686  psgnfzto1stlem  33064  cycpmrn  33107  rmfsupp2  33200  pidlnzb  33382  drngidlhash  33394  extdgfialglem2  33701  constrsqrtcl  33787  qqhval2lem  33989  derangenlem  35203  subfacp1lem5  35216  btwndiff  36060  btwnconn1lem7  36126  btwnconn1lem12  36131  tan2h  37651  poimirlem1  37660  poimirlem9  37668  poimirlem17  37676  poimirlem22  37681  areacirclem1  37747  isdrngo2  37997  isdrngo3  37998  lsatn0  39037  lsatspn0  39038  lkrlspeqN  39209  cvlsupr2  39381  dalem25  39736  4atexlemcnd  40110  ltrncnvnid  40165  trlator0  40209  ltrnnidn  40212  trlnid  40217  cdleme3b  40267  cdleme11l  40307  cdleme16b  40317  cdleme35h2  40495  cdleme38n  40502  cdlemg8c  40667  cdlemg11a  40675  cdlemg12e  40685  cdlemg18a  40716  trlcoat  40761  trlcone  40766  tendo1ne0  40866  cdleml9  41022  dvheveccl  41150  dihmeetlem13N  41357  dihlspsnat  41371  dihpN  41374  dihatexv  41376  dochsat  41421  dochkrshp  41424  dochkr1  41516  lcfrlem28  41608  lcfrlem32  41612  mapdn0  41707  mapdpglem11  41720  mapdpglem16  41725  sticksstones1  42178  sn-1ne2  42297  pell1234qrne0  42885  jm2.26lem3  43033  2zrngnmlid  48285  2zrngnmrid  48286  2zrngnmlid2  48287  domnmsuppn0  48399  rmsuppss  48400  scmsuppss  48401  rrx2linest  48773  itscnhlinecirc02p  48816  inlinecirc02plem  48817  aacllem  49832