Theorem necon3d 3037

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  pm13.18OLD  3098  pssdifn0  4325  ssn0  4354  uniintsn  4913  funopsn  6910  f1prex  7040  ressuppssdif  7851  suppfnss  7855  suppssov1  7862  suppssfv  7866  omord  8194  nnmord  8258  mapdom2  8688  findcard2  8758  kmlem9  9584  isf32lem7  9781  1re  10641  addid1  10820  addn0nid  11060  nn0n0n1ge2  11963  xnegdi  12642  fseqsupubi  13347  sqrtgt0  14618  supcvg  15211  ntrivcvgfvn0  15255  efne0  15450  divgcdcoprmex  16010  pceulem  16182  pcqmul  16190  pcqcl  16193  pcaddlem  16224  pcadd  16225  grpinvnz  18170  symgfvne  18509  symg2bas  18521  odmulgeq  18684  gsumval3lem2  19026  gsumval3  19027  ring1ne0  19341  abvdom  19609  lmodfopne  19672  mptscmfsupp0  19699  lmodindp1  19786  lspsneleq  19887  lspsneq  19894  lspexch  19901  lspindp3  19908  lspsnsubn0  19912  ringelnzr  20039  0ringnnzr  20042  coe1tmmul2  20444  ply1scln0  20459  dsmmsubg  20887  dsmmlss  20888  elfrlmbasn0  20907  mavmulsolcl  21160  0ntr  21679  elcls3  21691  neindisj  21725  neindisj2  21731  conndisj  22024  dfconn2  22027  fbunfip  22477  deg1mul2  24708  ply1nzb  24716  ne0p  24797  dgreq0  24855  dgradd2  24858  dgrcolem2  24864  elqaalem3  24910  logcj  25189  argimgt0  25195  tanarg  25202  cxpsqrtth  25312  dvcnsqrt  25325  ang180lem2  25388  ftalem2  25651  ftalem4  25653  ftalem5  25654  dvdssqf  25715  lmimid  26580  lmiisolem  26582  hypcgrlem1  26585  hypcgrlem2  26586  f1otrg  26657  f1otrge  26658  ax5seglem4  26718  ax5seglem5  26719  axeuclid  26749  axcontlem2  26751  axcontlem4  26753  pthdivtx  27510  spthdep  27515  usgr2wlkneq  27537  usgr2trlncl  27541  clwwlkccat  27768  clwwlkwwlksb  27833  clwwlknonel  27874  3pthdlem1  27943  uhgr3cyclexlem  27960  frgrwopreglem4a  28089  frrusgrord0lem  28118  nmlno0lem  28570  hlipgt0  28691  h1dn0  29329  spansneleq  29347  h1datomi  29358  nmlnop0iALT  29772  superpos  30131  chirredi  30171  preimane  30415  ogrpaddlt  30718  psgnfzto1stlem  30742  cycpmrn  30785  rmfsupp2  30866  qqhval2lem  31222  derangenlem  32418  subfacp1lem5  32431  scutbdaylt  33276  btwndiff  33488  btwnconn1lem7  33554  btwnconn1lem12  33559  tan2h  34899  poimirlem1  34908  poimirlem9  34916  poimirlem17  34924  poimirlem22  34929  areacirclem1  34997  isdrngo2  35251  isdrngo3  35252  lsatn0  36150  lsatspn0  36151  lkrlspeqN  36322  cvlsupr2  36494  dalem25  36849  4atexlemcnd  37223  ltrncnvnid  37278  trlator0  37322  ltrnnidn  37325  trlnid  37330  cdleme3b  37380  cdleme11l  37420  cdleme16b  37430  cdleme35h2  37608  cdleme38n  37615  cdlemg8c  37780  cdlemg11a  37788  cdlemg12e  37798  cdlemg18a  37829  trlcoat  37874  trlcone  37879  tendo1ne0  37979  cdleml9  38135  dvheveccl  38263  dihmeetlem13N  38470  dihlspsnat  38484  dihpN  38487  dihatexv  38489  dochsat  38534  dochkrshp  38537  dochkr1  38629  lcfrlem28  38721  lcfrlem32  38725  mapdn0  38820  mapdpglem11  38833  mapdpglem16  38838  sn-1ne2  39207  pell1234qrne0  39499  jm2.26lem3  39647  2zrngnmlid  44269  2zrngnmrid  44270  2zrngnmlid2  44271  domnmsuppn0  44466  rmsuppss  44467  scmsuppss  44469  rrx2linest  44778  itscnhlinecirc02p  44821  inlinecirc02plem  44822  aacllem  44951