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 1533   ≠ 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  4906  funopsn  6905  f1prex  7034  ressuppssdif  7845  suppfnss  7849  suppssov1  7856  suppssfv  7860  omord  8188  nnmord  8252  mapdom2  8682  findcard2  8752  kmlem9  9578  isf32lem7  9775  1re  10635  addid1  10814  addn0nid  11054  nn0n0n1ge2  11956  xnegdi  12635  fseqsupubi  13340  sqrtgt0  14612  supcvg  15205  ntrivcvgfvn0  15249  efne0  15444  divgcdcoprmex  16004  pceulem  16176  pcqmul  16184  pcqcl  16187  pcaddlem  16218  pcadd  16219  grpinvnz  18164  symgfvne  18503  symg2bas  18515  odmulgeq  18678  gsumval3lem2  19020  gsumval3  19021  ring1ne0  19335  abvdom  19603  lmodfopne  19666  mptscmfsupp0  19693  lmodindp1  19780  lspsneleq  19881  lspsneq  19888  lspexch  19895  lspindp3  19902  lspsnsubn0  19906  ringelnzr  20033  0ringnnzr  20036  coe1tmmul2  20438  ply1scln0  20453  dsmmsubg  20881  dsmmlss  20882  elfrlmbasn0  20901  mavmulsolcl  21154  0ntr  21673  elcls3  21685  neindisj  21719  neindisj2  21725  conndisj  22018  dfconn2  22021  fbunfip  22471  deg1mul2  24702  ply1nzb  24710  ne0p  24791  dgreq0  24849  dgradd2  24852  dgrcolem2  24858  elqaalem3  24904  logcj  25183  argimgt0  25189  tanarg  25196  cxpsqrtth  25306  dvcnsqrt  25319  ang180lem2  25382  ftalem2  25645  ftalem4  25647  ftalem5  25648  dvdssqf  25709  lmimid  26574  lmiisolem  26576  hypcgrlem1  26579  hypcgrlem2  26580  f1otrg  26651  f1otrge  26652  ax5seglem4  26712  ax5seglem5  26713  axeuclid  26743  axcontlem2  26745  axcontlem4  26747  pthdivtx  27504  spthdep  27509  usgr2wlkneq  27531  usgr2trlncl  27535  clwwlkccat  27762  clwwlkwwlksb  27827  clwwlknonel  27868  3pthdlem1  27937  uhgr3cyclexlem  27954  frgrwopreglem4a  28083  frrusgrord0lem  28112  nmlno0lem  28564  hlipgt0  28685  h1dn0  29323  spansneleq  29341  h1datomi  29352  nmlnop0iALT  29766  superpos  30125  chirredi  30165  preimane  30409  ogrpaddlt  30713  psgnfzto1stlem  30737  cycpmrn  30780  rmfsupp2  30861  qqhval2lem  31217  derangenlem  32413  subfacp1lem5  32426  scutbdaylt  33271  btwndiff  33483  btwnconn1lem7  33549  btwnconn1lem12  33554  tan2h  34878  poimirlem1  34887  poimirlem9  34895  poimirlem17  34903  poimirlem22  34908  areacirclem1  34976  isdrngo2  35230  isdrngo3  35231  lsatn0  36129  lsatspn0  36130  lkrlspeqN  36301  cvlsupr2  36473  dalem25  36828  4atexlemcnd  37202  ltrncnvnid  37257  trlator0  37301  ltrnnidn  37304  trlnid  37309  cdleme3b  37359  cdleme11l  37399  cdleme16b  37409  cdleme35h2  37587  cdleme38n  37594  cdlemg8c  37759  cdlemg11a  37767  cdlemg12e  37777  cdlemg18a  37808  trlcoat  37853  trlcone  37858  tendo1ne0  37958  cdleml9  38114  dvheveccl  38242  dihmeetlem13N  38449  dihlspsnat  38463  dihpN  38466  dihatexv  38468  dochsat  38513  dochkrshp  38516  dochkr1  38608  lcfrlem28  38700  lcfrlem32  38704  mapdn0  38799  mapdpglem11  38812  mapdpglem16  38817  sn-1ne2  39151  pell1234qrne0  39443  jm2.26lem3  39591  2zrngnmlid  44213  2zrngnmrid  44214  2zrngnmlid2  44215  domnmsuppn0  44410  rmsuppss  44411  scmsuppss  44413  rrx2linest  44722  itscnhlinecirc02p  44765  inlinecirc02plem  44766  aacllem  44895