Theorem necon3d 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  pssdifn0  4366  ssn0  4401  uniintsn  4992  funopsn  7146  f1prex  7282  poxp3  8136  ressuppssdif  8170  suppfnss  8174  suppssov1  8183  suppssfv  8187  omord  8568  nnmord  8632  mapdom2  9148  findcard2OLD  9284  kmlem9  10153  isf32lem7  10354  1re  11214  addrid  11394  addn0nid  11634  nn0n0n1ge2  12539  xnegdi  13227  fseqsupubi  13943  sqrtgt0  15205  supcvg  15802  ntrivcvgfvn0  15845  efne0  16040  divgcdcoprmex  16603  pceulem  16778  pcqmul  16786  pcqcl  16789  pcaddlem  16821  pcadd  16822  grpinvnz  18894  symgfvne  19248  symg2bas  19260  odmulgeq  19425  gsumval3lem2  19774  gsumval3  19775  ring1ne0  20111  ringelnzr  20300  0ringnnzr  20302  abvdom  20446  lmodfopne  20510  mptscmfsupp0  20537  lmodindp1  20625  lspsneleq  20728  lspsneq  20735  lspexch  20742  lspindp3  20749  lspsnsubn0  20753  dsmmsubg  21298  dsmmlss  21299  elfrlmbasn0  21318  coe1tmmul2  21798  ply1scln0  21814  mavmulsolcl  22053  0ntr  22575  elcls3  22587  neindisj  22621  neindisj2  22627  conndisj  22920  dfconn2  22923  fbunfip  23373  deg1mul2  25632  ply1nzb  25640  ne0p  25721  dgreq0  25779  dgradd2  25782  dgrcolem2  25788  elqaalem3  25834  logcj  26114  argimgt0  26120  tanarg  26127  cxpsqrtth  26238  dvcnsqrt  26252  ang180lem2  26315  ftalem2  26578  ftalem4  26580  ftalem5  26581  dvdssqf  26642  scutbdaylt  27320  lmimid  28076  lmiisolem  28078  hypcgrlem1  28081  hypcgrlem2  28082  f1otrg  28153  f1otrge  28154  ax5seglem4  28221  ax5seglem5  28222  axeuclid  28252  axcontlem2  28254  axcontlem4  28256  pthdivtx  29017  spthdep  29022  usgr2wlkneq  29044  usgr2trlncl  29048  clwwlkccat  29274  clwwlkwwlksb  29338  clwwlknonel  29379  3pthdlem1  29448  uhgr3cyclexlem  29465  frgrwopreglem4a  29594  frrusgrord0lem  29623  nmlno0lem  30077  hlipgt0  30198  h1dn0  30836  spansneleq  30854  h1datomi  30865  nmlnop0iALT  31279  superpos  31638  chirredi  31678  preimane  31926  preiman0  31962  ogrpaddlt  32266  psgnfzto1stlem  32290  cycpmrn  32333  rmfsupp2  32418  pidlnzb  32571  drngidlhash  32583  qqhval2lem  32992  derangenlem  34193  subfacp1lem5  34206  btwndiff  35030  btwnconn1lem7  35096  btwnconn1lem12  35101  tan2h  36528  poimirlem1  36537  poimirlem9  36545  poimirlem17  36553  poimirlem22  36558  areacirclem1  36624  isdrngo2  36874  isdrngo3  36875  lsatn0  37917  lsatspn0  37918  lkrlspeqN  38089  cvlsupr2  38261  dalem25  38617  4atexlemcnd  38991  ltrncnvnid  39046  trlator0  39090  ltrnnidn  39093  trlnid  39098  cdleme3b  39148  cdleme11l  39188  cdleme16b  39198  cdleme35h2  39376  cdleme38n  39383  cdlemg8c  39548  cdlemg11a  39556  cdlemg12e  39566  cdlemg18a  39597  trlcoat  39642  trlcone  39647  tendo1ne0  39747  cdleml9  39903  dvheveccl  40031  dihmeetlem13N  40238  dihlspsnat  40252  dihpN  40255  dihatexv  40257  dochsat  40302  dochkrshp  40305  dochkr1  40397  lcfrlem28  40489  lcfrlem32  40493  mapdn0  40588  mapdpglem11  40601  mapdpglem16  40606  sticksstones1  41010  sn-1ne2  41227  pell1234qrne0  41639  jm2.26lem3  41788  2zrngnmlid  46895  2zrngnmrid  46896  2zrngnmlid2  46897  domnmsuppn0  47093  rmsuppss  47094  scmsuppss  47096  rrx2linest  47476  itscnhlinecirc02p  47519  inlinecirc02plem  47520  aacllem  47896