Theorem necon3d 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  pssdifn0  4309  ssn0  4345  uniintsn  4928  funopsn  7095  dff14i  7207  f1prex  7232  poxp3  8093  ressuppssdif  8128  suppfnss  8132  suppssov1  8140  suppssov2  8141  suppssfv  8145  omord  8496  nnmord  8561  mapdom2  9079  kmlem9  10072  isf32lem7  10272  1re  11135  addrid  11317  addn0nid  11561  nn0n0n1ge2  12496  xnegdi  13191  fseqsupubi  13931  sqrtgt0  15211  supcvg  15812  ntrivcvgfvn0  15855  efne0d  16053  efne0OLD  16055  divgcdcoprmex  16626  pceulem  16807  pcqmul  16815  pcqcl  16818  pcaddlem  16850  pcadd  16851  grpinvnz  18977  symgfvne  19347  symg2bas  19359  odmulgeq  19523  gsumval3lem2  19872  gsumval3  19873  ogrpaddlt  20104  ring1ne0  20271  ringelnzr  20491  0ringnnzr  20493  abvdom  20798  lmodfopne  20886  mptscmfsupp0  20913  lmodindp1  21000  lspsneleq  21105  lspsneq  21112  lspexch  21119  lspindp3  21126  lspsnsubn0  21130  dsmmsubg  21733  dsmmlss  21734  elfrlmbasn0  21753  coe1tmmul2  22251  ply1scln0  22266  mavmulsolcl  22526  0ntr  23046  elcls3  23058  neindisj  23092  neindisj2  23098  conndisj  23391  dfconn2  23394  fbunfip  23844  deg1mul2  26089  ply1nzb  26098  ne0p  26182  dgreq0  26240  dgradd2  26243  dgrcolem2  26249  elqaalem3  26298  logcj  26583  argimgt0  26589  tanarg  26596  cxpsqrtth  26707  dvcnsqrt  26721  ang180lem2  26787  ftalem2  27051  ftalem4  27053  ftalem5  27054  dvdssqf  27115  cutbdaylt  27804  expsne0  28442  lmimid  28876  lmiisolem  28878  hypcgrlem1  28881  hypcgrlem2  28882  f1otrg  28953  f1otrge  28954  ax5seglem4  29015  ax5seglem5  29016  axeuclid  29046  axcontlem2  29048  axcontlem4  29050  pthdivtx  29810  spthdep  29817  usgr2wlkneq  29839  usgr2trlncl  29843  clwwlkccat  30075  clwwlkwwlksb  30139  clwwlknonel  30180  3pthdlem1  30249  uhgr3cyclexlem  30266  frgrwopreglem4a  30395  frrusgrord0lem  30424  nmlno0lem  30879  hlipgt0  31000  h1dn0  31638  spansneleq  31656  h1datomi  31667  nmlnop0iALT  32081  superpos  32440  chirredi  32480  preimane  32757  preiman0  32798  psgnfzto1stlem  33176  cycpmrn  33219  rmfsupp2  33314  pidlnzb  33497  drngidlhash  33509  extdgfialglem2  33853  constrsqrtcl  33939  qqhval2lem  34141  derangenlem  35369  subfacp1lem5  35382  btwndiff  36225  btwnconn1lem7  36291  btwnconn1lem12  36296  mh-inf3f1  36739  tan2h  37947  poimirlem1  37956  poimirlem9  37964  poimirlem17  37972  poimirlem22  37977  areacirclem1  38043  isdrngo2  38293  isdrngo3  38294  lsatn0  39459  lsatspn0  39460  lkrlspeqN  39631  cvlsupr2  39803  dalem25  40158  4atexlemcnd  40532  ltrncnvnid  40587  trlator0  40631  ltrnnidn  40634  trlnid  40639  cdleme3b  40689  cdleme11l  40729  cdleme16b  40739  cdleme35h2  40917  cdleme38n  40924  cdlemg8c  41089  cdlemg11a  41097  cdlemg12e  41107  cdlemg18a  41138  trlcoat  41183  trlcone  41188  tendo1ne0  41288  cdleml9  41444  dvheveccl  41572  dihmeetlem13N  41779  dihlspsnat  41793  dihpN  41796  dihatexv  41798  dochsat  41843  dochkrshp  41846  dochkr1  41938  lcfrlem28  42030  lcfrlem32  42034  mapdn0  42129  mapdpglem11  42142  mapdpglem16  42147  sticksstones1  42599  sn-1ne2  42717  pell1234qrne0  43299  jm2.26lem3  43447  2zrngnmlid  48743  2zrngnmrid  48744  2zrngnmlid2  48745  domnmsuppn0  48857  rmsuppss  48858  scmsuppss  48859  rrx2linest  49230  itscnhlinecirc02p  49273  inlinecirc02plem  49274  aacllem  50288