Theorem necon3d 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ≠ wne 2932

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 210  df-ne 2933

This theorem is referenced by:  pssdifn0  4266  ssn0  4301  uniintsn  4884  funopsn  6941  f1prex  7072  ressuppssdif  7905  suppfnss  7909  suppssov1  7918  suppssfv  7922  omord  8274  nnmord  8338  mapdom2  8795  findcard2OLD  8891  kmlem9  9737  isf32lem7  9938  1re  10798  addid1  10977  addn0nid  11217  nn0n0n1ge2  12122  xnegdi  12803  fseqsupubi  13516  sqrtgt0  14787  supcvg  15383  ntrivcvgfvn0  15426  efne0  15621  divgcdcoprmex  16186  pceulem  16361  pcqmul  16369  pcqcl  16372  pcaddlem  16404  pcadd  16405  grpinvnz  18388  symgfvne  18727  symg2bas  18739  odmulgeq  18902  gsumval3lem2  19245  gsumval3  19246  ring1ne0  19563  abvdom  19828  lmodfopne  19891  mptscmfsupp0  19918  lmodindp1  20005  lspsneleq  20106  lspsneq  20113  lspexch  20120  lspindp3  20127  lspsnsubn0  20131  ringelnzr  20258  0ringnnzr  20261  dsmmsubg  20659  dsmmlss  20660  elfrlmbasn0  20679  coe1tmmul2  21151  ply1scln0  21166  mavmulsolcl  21402  0ntr  21922  elcls3  21934  neindisj  21968  neindisj2  21974  conndisj  22267  dfconn2  22270  fbunfip  22720  deg1mul2  24966  ply1nzb  24974  ne0p  25055  dgreq0  25113  dgradd2  25116  dgrcolem2  25122  elqaalem3  25168  logcj  25448  argimgt0  25454  tanarg  25461  cxpsqrtth  25571  dvcnsqrt  25584  ang180lem2  25647  ftalem2  25910  ftalem4  25912  ftalem5  25913  dvdssqf  25974  lmimid  26839  lmiisolem  26841  hypcgrlem1  26844  hypcgrlem2  26845  f1otrg  26916  f1otrge  26917  ax5seglem4  26977  ax5seglem5  26978  axeuclid  27008  axcontlem2  27010  axcontlem4  27012  pthdivtx  27770  spthdep  27775  usgr2wlkneq  27797  usgr2trlncl  27801  clwwlkccat  28027  clwwlkwwlksb  28091  clwwlknonel  28132  3pthdlem1  28201  uhgr3cyclexlem  28218  frgrwopreglem4a  28347  frrusgrord0lem  28376  nmlno0lem  28828  hlipgt0  28949  h1dn0  29587  spansneleq  29605  h1datomi  29616  nmlnop0iALT  30030  superpos  30389  chirredi  30429  preimane  30681  preiman0  30716  ogrpaddlt  31016  psgnfzto1stlem  31040  cycpmrn  31083  rmfsupp2  31165  qqhval2lem  31597  derangenlem  32800  subfacp1lem5  32813  scutbdaylt  33698  btwndiff  34015  btwnconn1lem7  34081  btwnconn1lem12  34086  tan2h  35455  poimirlem1  35464  poimirlem9  35472  poimirlem17  35480  poimirlem22  35485  areacirclem1  35551  isdrngo2  35802  isdrngo3  35803  lsatn0  36699  lsatspn0  36700  lkrlspeqN  36871  cvlsupr2  37043  dalem25  37398  4atexlemcnd  37772  ltrncnvnid  37827  trlator0  37871  ltrnnidn  37874  trlnid  37879  cdleme3b  37929  cdleme11l  37969  cdleme16b  37979  cdleme35h2  38157  cdleme38n  38164  cdlemg8c  38329  cdlemg11a  38337  cdlemg12e  38347  cdlemg18a  38378  trlcoat  38423  trlcone  38428  tendo1ne0  38528  cdleml9  38684  dvheveccl  38812  dihmeetlem13N  39019  dihlspsnat  39033  dihpN  39036  dihatexv  39038  dochsat  39083  dochkrshp  39086  dochkr1  39178  lcfrlem28  39270  lcfrlem32  39274  mapdn0  39369  mapdpglem11  39382  mapdpglem16  39387  sticksstones1  39771  sn-1ne2  39943  pell1234qrne0  40319  jm2.26lem3  40467  2zrngnmlid  45123  2zrngnmrid  45124  2zrngnmlid2  45125  domnmsuppn0  45321  rmsuppss  45322  scmsuppss  45324  rrx2linest  45704  itscnhlinecirc02p  45747  inlinecirc02plem  45748  aacllem  46119