Theorem necon3d 2977

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  pssdifn0  4320  ssn0  4357  uniintsn  4942  funopsnOLD  7127  dff14i  7239  f1prex  7264  poxp3  8125  ressuppssdif  8160  suppfnss  8164  suppssov1  8172  suppssov2  8173  suppssfv  8177  omord  8532  nnmord  8597  mapdom2  9116  kmlem9  10112  isf32lem7  10313  1re  11178  addrid  11360  addn0nid  11604  nn0n0n1ge2  12546  xnegdi  13248  fseqsupubi  13988  sqrtgt0  15268  supcvg  15869  ntrivcvgfvn0  15912  efne0d  16110  efne0OLD  16112  divgcdcoprmex  16683  pceulem  16864  pcqmul  16872  pcqcl  16875  pcaddlem  16907  pcadd  16908  grpinvnz  19035  symgfvne  19404  symg2bas  19416  odmulgeq  19580  gsumval3lem2  19929  gsumval3  19930  ogrpaddlt  20161  ring1ne0  20328  ringelnzr  20552  0ringnnzr  20554  abvdom  20859  lmodfopne  20947  mptscmfsupp0  20974  lmodindp1  21061  lspsneleq  21165  lspsneq  21172  lspexch  21179  lspindp3  21186  lspsnsubn0  21190  dsmmsubg  21775  dsmmlss  21776  elfrlmbasn0  21795  coe1tmmul2  22319  ply1scln0  22334  mavmulsolcl  22591  0ntr  23111  elcls3  23123  neindisj  23157  neindisj2  23163  conndisj  23456  dfconn2  23459  fbunfip  23909  deg1mul2  26154  ply1nzb  26163  ne0p  26247  dgreq0  26305  dgradd2  26308  dgrcolem2  26314  elqaalem3  26362  logcj  26648  argimgt0  26654  tanarg  26661  cxpsqrtth  26772  dvcnsqrt  26786  ang180lem2  26852  ftalem2  27115  ftalem4  27117  ftalem5  27118  dvdssqf  27179  cutbdaylt  27868  expsne0  28506  lmimid  28940  lmiisolem  28942  hypcgrlem1  28945  hypcgrlem2  28946  f1otrg  29017  f1otrge  29018  ax5seglem4  29079  ax5seglem5  29080  axeuclid  29110  axcontlem2  29112  axcontlem4  29114  pthdivtx  29873  spthdep  29880  usgr2wlkneq  29902  usgr2trlncl  29906  clwwlkccat  30138  clwwlkwwlksb  30202  clwwlknonel  30243  3pthdlem1  30312  uhgr3cyclexlem  30329  frgrwopreglem4a  30458  frrusgrord0lem  30487  nmlno0lem  30942  hlipgt0  31063  h1dn0  31701  spansneleq  31719  h1datomi  31730  nmlnop0iALT  32144  superpos  32503  chirredi  32543  preimane  32821  preiman0  32862  psgnfzto1stlem  33241  cycpmrn  33284  rmfsupp2  33379  pidlnzb  33569  drngidlhash  33581  extdgfialglem2  33951  constrsqrtcl  34037  qqhval2lem  34239  derangenlem  35485  subfacp1lem5  35498  btwndiff  36341  btwnconn1lem7  36407  btwnconn1lem12  36412  mh-inf3f1  36865  tan2h  38075  poimirlem1  38084  poimirlem9  38092  poimirlem17  38100  poimirlem22  38105  areacirclem1  38171  isdrngo2  38421  isdrngo3  38422  lsatn0  39587  lsatspn0  39588  lkrlspeqN  39759  cvlsupr2  39931  dalem25  40286  4atexlemcnd  40660  ltrncnvnid  40715  trlator0  40759  ltrnnidn  40762  trlnid  40767  cdleme3b  40817  cdleme11l  40857  cdleme16b  40867  cdleme35h2  41045  cdleme38n  41052  cdlemg8c  41217  cdlemg11a  41225  cdlemg12e  41235  cdlemg18a  41266  trlcoat  41311  trlcone  41316  tendo1ne0  41416  cdleml9  41572  dvheveccl  41700  dihmeetlem13N  41907  dihlspsnat  41921  dihpN  41924  dihatexv  41926  dochsat  41971  dochkrshp  41974  dochkr1  42066  lcfrlem28  42158  lcfrlem32  42162  mapdn0  42257  mapdpglem11  42270  mapdpglem16  42275  sticksstones1  42727  sn-1ne2  42844  pell1234qrne0  43394  jm2.26lem3  43542  2zrngnmlid  48841  2zrngnmrid  48842  2zrngnmlid2  48843  domnmsuppn0  48955  rmsuppss  48956  scmsuppss  48957  rrx2linest  49328  itscnhlinecirc02p  49371  inlinecirc02plem  49372  aacllem  50386