Theorem necon3d 2803

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  pm13.18  2863  pssdifn0  3898  ssn0  3928  uniintsn  4449  funopsn  6319  f1prex  6439  ressuppssdif  7203  suppfnss  7207  suppssov1  7214  suppssfv  7218  omord  7535  nnmord  7599  mapdom2  8016  findcard2  8085  kmlem9  8863  isf32lem7  9064  1re  9918  addid1  10095  addn0nid  10330  nn0n0n1ge2  11235  xnegdi  11950  fseqsupubi  12639  sqrtgt0  13847  supcvg  14427  ntrivcvgfvn0  14470  efne0  14666  divgcdcoprmex  15218  pceulem  15388  pcqmul  15396  pcqcl  15399  pcaddlem  15430  pcadd  15431  grpinvnz  17309  symgfvne  17631  symg2bas  17641  odmulgeq  17797  gsumval3lem2  18130  gsumval3  18131  ring1ne0  18414  abvdom  18661  lmodfopne  18724  mptscmfsupp0  18751  lmodindp1  18835  lspsneleq  18936  lspsneq  18943  lspexch  18950  lspindp3  18957  lspsnsubn0  18961  ringelnzr  19087  0ringnnzr  19090  coe1tmmul2  19467  ply1scln0  19482  dsmmsubg  19906  dsmmlss  19907  elfrlmbasn0  19925  mavmulsolcl  20176  0ntr  20685  elcls3  20697  neindisj  20731  neindisj2  20737  conndisj  21029  dfcon2  21032  fbunfip  21483  deg1mul2  23678  ply1nzb  23686  ne0p  23767  dgreq0  23825  dgradd2  23828  dgrcolem2  23834  elqaalem3  23880  logcj  24156  argimgt0  24162  tanarg  24169  dvcnsqrt  24285  ang180lem2  24340  ftalem2  24600  ftalem4  24602  ftalem5  24603  dvdssqf  24664  mirhl2  25376  lmimid  25486  lmiisolem  25488  hypcgrlem1  25491  hypcgrlem2  25492  f1otrg  25551  f1otrge  25552  ax5seglem4  25612  ax5seglem5  25613  axeuclid  25643  axcontlem2  25645  axcontlem4  25647  usgra2adedgspthlem2  26140  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  frgregordn0  26597  nmlno0lem  27032  hlipgt0  27154  h1dn0  27795  spansneleq  27813  h1datomi  27824  nmlnop0iALT  28238  superpos  28597  chirredi  28637  ogrpaddlt  29049  psgnfzto1stlem  29181  qqhval2lem  29353  derangenlem  30407  subfacp1lem5  30420  btwndiff  31304  btwnconn1lem7  31370  btwnconn1lem12  31375  tan2h  32571  poimirlem1  32580  poimirlem9  32588  poimirlem17  32596  poimirlem22  32601  areacirclem1  32670  isdrngo2  32927  isdrngo3  32928  lsatn0  33304  lsatspn0  33305  lkrlspeqN  33476  cvlsupr2  33648  dalem25  34002  4atexlemcnd  34376  ltrncnvnid  34431  trlator0  34476  ltrnnidn  34479  trlnid  34484  cdleme3b  34534  cdleme11l  34574  cdleme16b  34584  cdleme35h2  34763  cdleme38n  34770  cdlemg8c  34935  cdlemg11a  34943  cdlemg12e  34953  cdlemg18a  34984  trlcoat  35029  trlcone  35034  tendo1ne0  35134  cdleml9  35290  dvheveccl  35419  dihmeetlem13N  35626  dihlspsnat  35640  dihpN  35643  dihatexv  35645  dochsat  35690  dochkrshp  35693  dochkr1  35785  lcfrlem28  35877  lcfrlem32  35881  mapdn0  35976  mapdpglem11  35989  mapdpglem16  35994  pell1234qrne0  36435  jm2.26lem3  36586  pthdivtx  40935  spthdep  40940  usgr2wlkneq  40962  usgr2trlncl  40966  3pthdlem1  41331  uhgr3cyclexlem  41348  frrusgrord0  41503  2zrngnmlid  41739  2zrngnmrid  41740  2zrngnmlid2  41741  domnmsuppn0  41944  rmsuppss  41945  scmsuppss  41947  aacllem  42356