Theorem necon3d 2963

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  pssdifn0  4296  ssn0  4331  uniintsn  4915  funopsn  7002  f1prex  7136  ressuppssdif  7972  suppfnss  7976  suppssov1  7985  suppssfv  7989  omord  8361  nnmord  8425  mapdom2  8884  findcard2OLD  8986  kmlem9  9845  isf32lem7  10046  1re  10906  addid1  11085  addn0nid  11325  nn0n0n1ge2  12230  xnegdi  12911  fseqsupubi  13626  sqrtgt0  14898  supcvg  15496  ntrivcvgfvn0  15539  efne0  15734  divgcdcoprmex  16299  pceulem  16474  pcqmul  16482  pcqcl  16485  pcaddlem  16517  pcadd  16518  grpinvnz  18561  symgfvne  18903  symg2bas  18915  odmulgeq  19079  gsumval3lem2  19422  gsumval3  19423  ring1ne0  19745  abvdom  20013  lmodfopne  20076  mptscmfsupp0  20103  lmodindp1  20191  lspsneleq  20292  lspsneq  20299  lspexch  20306  lspindp3  20313  lspsnsubn0  20317  ringelnzr  20450  0ringnnzr  20453  dsmmsubg  20860  dsmmlss  20861  elfrlmbasn0  20880  coe1tmmul2  21357  ply1scln0  21372  mavmulsolcl  21608  0ntr  22130  elcls3  22142  neindisj  22176  neindisj2  22182  conndisj  22475  dfconn2  22478  fbunfip  22928  deg1mul2  25184  ply1nzb  25192  ne0p  25273  dgreq0  25331  dgradd2  25334  dgrcolem2  25340  elqaalem3  25386  logcj  25666  argimgt0  25672  tanarg  25679  cxpsqrtth  25789  dvcnsqrt  25802  ang180lem2  25865  ftalem2  26128  ftalem4  26130  ftalem5  26131  dvdssqf  26192  lmimid  27059  lmiisolem  27061  hypcgrlem1  27064  hypcgrlem2  27065  f1otrg  27136  f1otrge  27137  ax5seglem4  27203  ax5seglem5  27204  axeuclid  27234  axcontlem2  27236  axcontlem4  27238  pthdivtx  27998  spthdep  28003  usgr2wlkneq  28025  usgr2trlncl  28029  clwwlkccat  28255  clwwlkwwlksb  28319  clwwlknonel  28360  3pthdlem1  28429  uhgr3cyclexlem  28446  frgrwopreglem4a  28575  frrusgrord0lem  28604  nmlno0lem  29056  hlipgt0  29177  h1dn0  29815  spansneleq  29833  h1datomi  29844  nmlnop0iALT  30258  superpos  30617  chirredi  30657  preimane  30909  preiman0  30944  ogrpaddlt  31245  psgnfzto1stlem  31269  cycpmrn  31312  rmfsupp2  31394  qqhval2lem  31831  derangenlem  33033  subfacp1lem5  33046  scutbdaylt  33939  btwndiff  34256  btwnconn1lem7  34322  btwnconn1lem12  34327  tan2h  35696  poimirlem1  35705  poimirlem9  35713  poimirlem17  35721  poimirlem22  35726  areacirclem1  35792  isdrngo2  36043  isdrngo3  36044  lsatn0  36940  lsatspn0  36941  lkrlspeqN  37112  cvlsupr2  37284  dalem25  37639  4atexlemcnd  38013  ltrncnvnid  38068  trlator0  38112  ltrnnidn  38115  trlnid  38120  cdleme3b  38170  cdleme11l  38210  cdleme16b  38220  cdleme35h2  38398  cdleme38n  38405  cdlemg8c  38570  cdlemg11a  38578  cdlemg12e  38588  cdlemg18a  38619  trlcoat  38664  trlcone  38669  tendo1ne0  38769  cdleml9  38925  dvheveccl  39053  dihmeetlem13N  39260  dihlspsnat  39274  dihpN  39277  dihatexv  39279  dochsat  39324  dochkrshp  39327  dochkr1  39419  lcfrlem28  39511  lcfrlem32  39515  mapdn0  39610  mapdpglem11  39623  mapdpglem16  39628  sticksstones1  40030  sn-1ne2  40216  pell1234qrne0  40591  jm2.26lem3  40739  2zrngnmlid  45395  2zrngnmrid  45396  2zrngnmlid2  45397  domnmsuppn0  45593  rmsuppss  45594  scmsuppss  45596  rrx2linest  45976  itscnhlinecirc02p  46019  inlinecirc02plem  46020  aacllem  46391