Theorem necon3d 2964

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

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

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 2944

This theorem is referenced by:  pssdifn0  4299  ssn0  4334  uniintsn  4918  funopsn  7020  f1prex  7156  ressuppssdif  8001  suppfnss  8005  suppssov1  8014  suppssfv  8018  omord  8399  nnmord  8463  mapdom2  8935  findcard2OLD  9056  kmlem9  9914  isf32lem7  10115  1re  10975  addid1  11155  addn0nid  11395  nn0n0n1ge2  12300  xnegdi  12982  fseqsupubi  13698  sqrtgt0  14970  supcvg  15568  ntrivcvgfvn0  15611  efne0  15806  divgcdcoprmex  16371  pceulem  16546  pcqmul  16554  pcqcl  16557  pcaddlem  16589  pcadd  16590  grpinvnz  18646  symgfvne  18988  symg2bas  19000  odmulgeq  19164  gsumval3lem2  19507  gsumval3  19508  ring1ne0  19830  abvdom  20098  lmodfopne  20161  mptscmfsupp0  20188  lmodindp1  20276  lspsneleq  20377  lspsneq  20384  lspexch  20391  lspindp3  20398  lspsnsubn0  20402  ringelnzr  20537  0ringnnzr  20540  dsmmsubg  20950  dsmmlss  20951  elfrlmbasn0  20970  coe1tmmul2  21447  ply1scln0  21462  mavmulsolcl  21700  0ntr  22222  elcls3  22234  neindisj  22268  neindisj2  22274  conndisj  22567  dfconn2  22570  fbunfip  23020  deg1mul2  25279  ply1nzb  25287  ne0p  25368  dgreq0  25426  dgradd2  25429  dgrcolem2  25435  elqaalem3  25481  logcj  25761  argimgt0  25767  tanarg  25774  cxpsqrtth  25884  dvcnsqrt  25897  ang180lem2  25960  ftalem2  26223  ftalem4  26225  ftalem5  26226  dvdssqf  26287  lmimid  27155  lmiisolem  27157  hypcgrlem1  27160  hypcgrlem2  27161  f1otrg  27232  f1otrge  27233  ax5seglem4  27300  ax5seglem5  27301  axeuclid  27331  axcontlem2  27333  axcontlem4  27335  pthdivtx  28097  spthdep  28102  usgr2wlkneq  28124  usgr2trlncl  28128  clwwlkccat  28354  clwwlkwwlksb  28418  clwwlknonel  28459  3pthdlem1  28528  uhgr3cyclexlem  28545  frgrwopreglem4a  28674  frrusgrord0lem  28703  nmlno0lem  29155  hlipgt0  29276  h1dn0  29914  spansneleq  29932  h1datomi  29943  nmlnop0iALT  30357  superpos  30716  chirredi  30756  preimane  31007  preiman0  31042  ogrpaddlt  31343  psgnfzto1stlem  31367  cycpmrn  31410  rmfsupp2  31492  qqhval2lem  31931  derangenlem  33133  subfacp1lem5  33146  scutbdaylt  34012  btwndiff  34329  btwnconn1lem7  34395  btwnconn1lem12  34400  tan2h  35769  poimirlem1  35778  poimirlem9  35786  poimirlem17  35794  poimirlem22  35799  areacirclem1  35865  isdrngo2  36116  isdrngo3  36117  lsatn0  37013  lsatspn0  37014  lkrlspeqN  37185  cvlsupr2  37357  dalem25  37712  4atexlemcnd  38086  ltrncnvnid  38141  trlator0  38185  ltrnnidn  38188  trlnid  38193  cdleme3b  38243  cdleme11l  38283  cdleme16b  38293  cdleme35h2  38471  cdleme38n  38478  cdlemg8c  38643  cdlemg11a  38651  cdlemg12e  38661  cdlemg18a  38692  trlcoat  38737  trlcone  38742  tendo1ne0  38842  cdleml9  38998  dvheveccl  39126  dihmeetlem13N  39333  dihlspsnat  39347  dihpN  39350  dihatexv  39352  dochsat  39397  dochkrshp  39400  dochkr1  39492  lcfrlem28  39584  lcfrlem32  39588  mapdn0  39683  mapdpglem11  39696  mapdpglem16  39701  sticksstones1  40102  sn-1ne2  40295  pell1234qrne0  40675  jm2.26lem3  40823  2zrngnmlid  45507  2zrngnmrid  45508  2zrngnmlid2  45509  domnmsuppn0  45705  rmsuppss  45706  scmsuppss  45708  rrx2linest  46088  itscnhlinecirc02p  46131  inlinecirc02plem  46132  aacllem  46505