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  27319  lmimid  28045  lmiisolem  28047  hypcgrlem1  28050  hypcgrlem2  28051  f1otrg  28122  f1otrge  28123  ax5seglem4  28190  ax5seglem5  28191  axeuclid  28221  axcontlem2  28223  axcontlem4  28225  pthdivtx  28986  spthdep  28991  usgr2wlkneq  29013  usgr2trlncl  29017  clwwlkccat  29243  clwwlkwwlksb  29307  clwwlknonel  29348  3pthdlem1  29417  uhgr3cyclexlem  29434  frgrwopreglem4a  29563  frrusgrord0lem  29592  nmlno0lem  30046  hlipgt0  30167  h1dn0  30805  spansneleq  30823  h1datomi  30834  nmlnop0iALT  31248  superpos  31607  chirredi  31647  preimane  31895  preiman0  31931  ogrpaddlt  32235  psgnfzto1stlem  32259  cycpmrn  32302  rmfsupp2  32387  pidlnzb  32540  drngidlhash  32552  qqhval2lem  32961  derangenlem  34162  subfacp1lem5  34175  btwndiff  34999  btwnconn1lem7  35065  btwnconn1lem12  35070  tan2h  36480  poimirlem1  36489  poimirlem9  36497  poimirlem17  36505  poimirlem22  36510  areacirclem1  36576  isdrngo2  36826  isdrngo3  36827  lsatn0  37869  lsatspn0  37870  lkrlspeqN  38041  cvlsupr2  38213  dalem25  38569  4atexlemcnd  38943  ltrncnvnid  38998  trlator0  39042  ltrnnidn  39045  trlnid  39050  cdleme3b  39100  cdleme11l  39140  cdleme16b  39150  cdleme35h2  39328  cdleme38n  39335  cdlemg8c  39500  cdlemg11a  39508  cdlemg12e  39518  cdlemg18a  39549  trlcoat  39594  trlcone  39599  tendo1ne0  39699  cdleml9  39855  dvheveccl  39983  dihmeetlem13N  40190  dihlspsnat  40204  dihpN  40207  dihatexv  40209  dochsat  40254  dochkrshp  40257  dochkr1  40349  lcfrlem28  40441  lcfrlem32  40445  mapdn0  40540  mapdpglem11  40553  mapdpglem16  40558  sticksstones1  40962  sn-1ne2  41179  pell1234qrne0  41591  jm2.26lem3  41740  2zrngnmlid  46847  2zrngnmrid  46848  2zrngnmlid2  46849  domnmsuppn0  47045  rmsuppss  47046  scmsuppss  47048  rrx2linest  47428  itscnhlinecirc02p  47471  inlinecirc02plem  47472  aacllem  47848