Theorem necon3d 2947

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

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

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 2927

This theorem is referenced by:  pssdifn0  4334  ssn0  4370  uniintsn  4952  funopsn  7123  dff14i  7237  f1prex  7262  poxp3  8132  ressuppssdif  8167  suppfnss  8171  suppssov1  8179  suppssov2  8180  suppssfv  8184  omord  8535  nnmord  8599  mapdom2  9118  kmlem9  10119  isf32lem7  10319  1re  11181  addrid  11361  addn0nid  11605  nn0n0n1ge2  12517  xnegdi  13215  fseqsupubi  13950  sqrtgt0  15231  supcvg  15829  ntrivcvgfvn0  15872  efne0d  16070  efne0OLD  16072  divgcdcoprmex  16643  pceulem  16823  pcqmul  16831  pcqcl  16834  pcaddlem  16866  pcadd  16867  grpinvnz  18949  symgfvne  19318  symg2bas  19330  odmulgeq  19494  gsumval3lem2  19843  gsumval3  19844  ring1ne0  20215  ringelnzr  20439  0ringnnzr  20441  abvdom  20746  lmodfopne  20813  mptscmfsupp0  20840  lmodindp1  20927  lspsneleq  21032  lspsneq  21039  lspexch  21046  lspindp3  21053  lspsnsubn0  21057  dsmmsubg  21659  dsmmlss  21660  elfrlmbasn0  21679  coe1tmmul2  22169  ply1scln0  22185  mavmulsolcl  22445  0ntr  22965  elcls3  22977  neindisj  23011  neindisj2  23017  conndisj  23310  dfconn2  23313  fbunfip  23763  deg1mul2  26026  ply1nzb  26035  ne0p  26119  dgreq0  26178  dgradd2  26181  dgrcolem2  26187  elqaalem3  26236  logcj  26522  argimgt0  26528  tanarg  26535  cxpsqrtth  26646  dvcnsqrt  26660  ang180lem2  26727  ftalem2  26991  ftalem4  26993  ftalem5  26994  dvdssqf  27055  scutbdaylt  27737  expsne0  28328  lmimid  28728  lmiisolem  28730  hypcgrlem1  28733  hypcgrlem2  28734  f1otrg  28805  f1otrge  28806  ax5seglem4  28866  ax5seglem5  28867  axeuclid  28897  axcontlem2  28899  axcontlem4  28901  pthdivtx  29664  spthdep  29671  usgr2wlkneq  29693  usgr2trlncl  29697  clwwlkccat  29926  clwwlkwwlksb  29990  clwwlknonel  30031  3pthdlem1  30100  uhgr3cyclexlem  30117  frgrwopreglem4a  30246  frrusgrord0lem  30275  nmlno0lem  30729  hlipgt0  30850  h1dn0  31488  spansneleq  31506  h1datomi  31517  nmlnop0iALT  31931  superpos  32290  chirredi  32330  preimane  32601  preiman0  32640  ogrpaddlt  33038  psgnfzto1stlem  33064  cycpmrn  33107  rmfsupp2  33196  pidlnzb  33400  drngidlhash  33412  constrsqrtcl  33776  qqhval2lem  33978  derangenlem  35165  subfacp1lem5  35178  btwndiff  36022  btwnconn1lem7  36088  btwnconn1lem12  36093  tan2h  37613  poimirlem1  37622  poimirlem9  37630  poimirlem17  37638  poimirlem22  37643  areacirclem1  37709  isdrngo2  37959  isdrngo3  37960  lsatn0  38999  lsatspn0  39000  lkrlspeqN  39171  cvlsupr2  39343  dalem25  39699  4atexlemcnd  40073  ltrncnvnid  40128  trlator0  40172  ltrnnidn  40175  trlnid  40180  cdleme3b  40230  cdleme11l  40270  cdleme16b  40280  cdleme35h2  40458  cdleme38n  40465  cdlemg8c  40630  cdlemg11a  40638  cdlemg12e  40648  cdlemg18a  40679  trlcoat  40724  trlcone  40729  tendo1ne0  40829  cdleml9  40985  dvheveccl  41113  dihmeetlem13N  41320  dihlspsnat  41334  dihpN  41337  dihatexv  41339  dochsat  41384  dochkrshp  41387  dochkr1  41479  lcfrlem28  41571  lcfrlem32  41575  mapdn0  41670  mapdpglem11  41683  mapdpglem16  41688  sticksstones1  42141  sn-1ne2  42260  pell1234qrne0  42848  jm2.26lem3  42997  2zrngnmlid  48247  2zrngnmrid  48248  2zrngnmlid2  48249  domnmsuppn0  48361  rmsuppss  48362  scmsuppss  48363  rrx2linest  48735  itscnhlinecirc02p  48778  inlinecirc02plem  48779  aacllem  49794