Theorem necon3d 2988

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 2980	. 2 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵))
3		df-ne 2968	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	syl6ibr 244	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1507   ≠ wne 2967

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 199  df-ne 2968

This theorem is referenced by:  pm13.18OLD  3049  pssdifn0  4213  ssn0  4241  uniintsn  4787  funopsn  6735  f1prex  6867  ressuppssdif  7656  suppfnss  7660  suppssov1  7667  suppssfv  7671  omord  7997  nnmord  8061  mapdom2  8486  findcard2  8555  kmlem9  9380  isf32lem7  9581  1re  10441  addid1  10622  addn0nid  10863  nn0n0n1ge2  11777  xnegdi  12460  fseqsupubi  13164  sqrtgt0  14482  supcvg  15074  ntrivcvgfvn0  15118  efne0  15313  divgcdcoprmex  15869  pceulem  16041  pcqmul  16049  pcqcl  16052  pcaddlem  16083  pcadd  16084  grpinvnz  17960  symgfvne  18280  symg2bas  18290  odmulgeq  18448  gsumval3lem2  18783  gsumval3  18784  ring1ne0  19067  abvdom  19334  lmodfopne  19397  mptscmfsupp0  19424  lmodindp1  19511  lspsneleq  19612  lspsneq  19619  lspexch  19626  lspindp3  19633  lspsnsubn0  19637  ringelnzr  19763  0ringnnzr  19766  coe1tmmul2  20150  ply1scln0  20165  dsmmsubg  20592  dsmmlss  20593  elfrlmbasn0  20612  mavmulsolcl  20867  0ntr  21386  elcls3  21398  neindisj  21432  neindisj2  21438  conndisj  21731  dfconn2  21734  fbunfip  22184  deg1mul2  24414  ply1nzb  24422  ne0p  24503  dgreq0  24561  dgradd2  24564  dgrcolem2  24570  elqaalem3  24616  logcj  24893  argimgt0  24899  tanarg  24906  cxpsqrtth  25016  dvcnsqrt  25029  ang180lem2  25092  ftalem2  25356  ftalem4  25358  ftalem5  25359  dvdssqf  25420  lmimid  26285  lmiisolem  26287  hypcgrlem1  26290  hypcgrlem2  26291  f1otrg  26363  f1otrge  26364  ax5seglem4  26424  ax5seglem5  26425  axeuclid  26455  axcontlem2  26457  axcontlem4  26459  pthdivtx  27221  spthdep  27226  usgr2wlkneq  27248  usgr2trlncl  27252  clwwlkccat  27499  clwwlkwwlksb  27580  clwwlknonel  27626  3pthdlem1  27696  uhgr3cyclexlem  27713  frgrwopreglem4a  27847  frrusgrord0lem  27876  nmlno0lem  28350  hlipgt0  28472  h1dn0  29113  spansneleq  29131  h1datomi  29142  nmlnop0iALT  29556  superpos  29915  chirredi  29955  preimane  30180  ogrpaddlt  30437  rmfsupp2  30545  psgnfzto1stlem  30691  qqhval2lem  30866  derangenlem  32003  subfacp1lem5  32016  scutbdaylt  32797  btwndiff  33009  btwnconn1lem7  33075  btwnconn1lem12  33080  tan2h  34325  poimirlem1  34334  poimirlem9  34342  poimirlem17  34350  poimirlem22  34355  areacirclem1  34423  isdrngo2  34678  isdrngo3  34679  lsatn0  35580  lsatspn0  35581  lkrlspeqN  35752  cvlsupr2  35924  dalem25  36279  4atexlemcnd  36653  ltrncnvnid  36708  trlator0  36752  ltrnnidn  36755  trlnid  36760  cdleme3b  36810  cdleme11l  36850  cdleme16b  36860  cdleme35h2  37038  cdleme38n  37045  cdlemg8c  37210  cdlemg11a  37218  cdlemg12e  37228  cdlemg18a  37259  trlcoat  37304  trlcone  37309  tendo1ne0  37409  cdleml9  37565  dvheveccl  37693  dihmeetlem13N  37900  dihlspsnat  37914  dihpN  37917  dihatexv  37919  dochsat  37964  dochkrshp  37967  dochkr1  38059  lcfrlem28  38151  lcfrlem32  38155  mapdn0  38250  mapdpglem11  38263  mapdpglem16  38268  pell1234qrne0  38846  jm2.26lem3  38994  2zrngnmlid  43585  2zrngnmrid  43586  2zrngnmlid2  43587  domnmsuppn0  43784  rmsuppss  43785  scmsuppss  43787  rrx2linest  44098  itscnhlinecirc02p  44141  inlinecirc02plem  44142  aacllem  44270