Theorem necon3d 2960

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2939

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 2940

This theorem is referenced by:  pssdifn0  4365  ssn0  4400  uniintsn  4991  funopsn  7148  f1prex  7285  poxp3  8140  ressuppssdif  8174  suppfnss  8178  suppssov1  8187  suppssfv  8191  omord  8572  nnmord  8636  mapdom2  9152  findcard2OLD  9288  kmlem9  10157  isf32lem7  10358  1re  11219  addrid  11399  addn0nid  11639  nn0n0n1ge2  12544  xnegdi  13232  fseqsupubi  13948  sqrtgt0  15210  supcvg  15807  ntrivcvgfvn0  15850  efne0  16045  divgcdcoprmex  16608  pceulem  16783  pcqmul  16791  pcqcl  16794  pcaddlem  16826  pcadd  16827  grpinvnz  18931  symgfvne  19290  symg2bas  19302  odmulgeq  19467  gsumval3lem2  19816  gsumval3  19817  ring1ne0  20188  ringelnzr  20413  0ringnnzr  20415  abvdom  20590  lmodfopne  20655  mptscmfsupp0  20682  lmodindp1  20770  lspsneleq  20874  lspsneq  20881  lspexch  20888  lspindp3  20895  lspsnsubn0  20899  dsmmsubg  21518  dsmmlss  21519  elfrlmbasn0  21538  coe1tmmul2  22019  ply1scln0  22035  mavmulsolcl  22274  0ntr  22796  elcls3  22808  neindisj  22842  neindisj2  22848  conndisj  23141  dfconn2  23144  fbunfip  23594  deg1mul2  25868  ply1nzb  25876  ne0p  25957  dgreq0  26016  dgradd2  26019  dgrcolem2  26025  elqaalem3  26071  logcj  26351  argimgt0  26357  tanarg  26364  cxpsqrtth  26475  dvcnsqrt  26489  ang180lem2  26552  ftalem2  26815  ftalem4  26817  ftalem5  26818  dvdssqf  26879  scutbdaylt  27557  lmimid  28313  lmiisolem  28315  hypcgrlem1  28318  hypcgrlem2  28319  f1otrg  28390  f1otrge  28391  ax5seglem4  28458  ax5seglem5  28459  axeuclid  28489  axcontlem2  28491  axcontlem4  28493  pthdivtx  29254  spthdep  29259  usgr2wlkneq  29281  usgr2trlncl  29285  clwwlkccat  29511  clwwlkwwlksb  29575  clwwlknonel  29616  3pthdlem1  29685  uhgr3cyclexlem  29702  frgrwopreglem4a  29831  frrusgrord0lem  29860  nmlno0lem  30314  hlipgt0  30435  h1dn0  31073  spansneleq  31091  h1datomi  31102  nmlnop0iALT  31516  superpos  31875  chirredi  31915  preimane  32163  preiman0  32199  ogrpaddlt  32506  psgnfzto1stlem  32530  cycpmrn  32573  rmfsupp2  32658  pidlnzb  32815  drngidlhash  32827  qqhval2lem  33260  derangenlem  34461  subfacp1lem5  34474  btwndiff  35304  btwnconn1lem7  35370  btwnconn1lem12  35375  tan2h  36784  poimirlem1  36793  poimirlem9  36801  poimirlem17  36809  poimirlem22  36814  areacirclem1  36880  isdrngo2  37130  isdrngo3  37131  lsatn0  38173  lsatspn0  38174  lkrlspeqN  38345  cvlsupr2  38517  dalem25  38873  4atexlemcnd  39247  ltrncnvnid  39302  trlator0  39346  ltrnnidn  39349  trlnid  39354  cdleme3b  39404  cdleme11l  39444  cdleme16b  39454  cdleme35h2  39632  cdleme38n  39639  cdlemg8c  39804  cdlemg11a  39812  cdlemg12e  39822  cdlemg18a  39853  trlcoat  39898  trlcone  39903  tendo1ne0  40003  cdleml9  40159  dvheveccl  40287  dihmeetlem13N  40494  dihlspsnat  40508  dihpN  40511  dihatexv  40513  dochsat  40558  dochkrshp  40561  dochkr1  40653  lcfrlem28  40745  lcfrlem32  40749  mapdn0  40844  mapdpglem11  40857  mapdpglem16  40862  sticksstones1  41269  sn-1ne2  41482  pell1234qrne0  41894  jm2.26lem3  42043  2zrngnmlid  46936  2zrngnmrid  46937  2zrngnmlid2  46938  domnmsuppn0  47134  rmsuppss  47135  scmsuppss  47137  rrx2linest  47516  itscnhlinecirc02p  47559  inlinecirc02plem  47560  aacllem  47936