Theorem necon3d 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  pssdifn0  4348  ssn0  4384  uniintsn  4966  funopsn  7143  dff14i  7257  f1prex  7282  poxp3  8154  ressuppssdif  8189  suppfnss  8193  suppssov1  8201  suppssov2  8202  suppssfv  8206  omord  8585  nnmord  8649  mapdom2  9167  kmlem9  10178  isf32lem7  10378  1re  11240  addrid  11420  addn0nid  11662  nn0n0n1ge2  12574  xnegdi  13269  fseqsupubi  14001  sqrtgt0  15282  supcvg  15877  ntrivcvgfvn0  15920  efne0d  16118  efne0OLD  16120  divgcdcoprmex  16690  pceulem  16870  pcqmul  16878  pcqcl  16881  pcaddlem  16913  pcadd  16914  grpinvnz  18998  symgfvne  19367  symg2bas  19379  odmulgeq  19543  gsumval3lem2  19892  gsumval3  19893  ring1ne0  20264  ringelnzr  20488  0ringnnzr  20490  abvdom  20795  lmodfopne  20862  mptscmfsupp0  20889  lmodindp1  20976  lspsneleq  21081  lspsneq  21088  lspexch  21095  lspindp3  21102  lspsnsubn0  21106  dsmmsubg  21708  dsmmlss  21709  elfrlmbasn0  21728  coe1tmmul2  22218  ply1scln0  22234  mavmulsolcl  22494  0ntr  23014  elcls3  23026  neindisj  23060  neindisj2  23066  conndisj  23359  dfconn2  23362  fbunfip  23812  deg1mul2  26076  ply1nzb  26085  ne0p  26169  dgreq0  26228  dgradd2  26231  dgrcolem2  26237  elqaalem3  26286  logcj  26572  argimgt0  26578  tanarg  26585  cxpsqrtth  26696  dvcnsqrt  26710  ang180lem2  26777  ftalem2  27041  ftalem4  27043  ftalem5  27044  dvdssqf  27105  scutbdaylt  27787  expsne0  28378  lmimid  28778  lmiisolem  28780  hypcgrlem1  28783  hypcgrlem2  28784  f1otrg  28855  f1otrge  28856  ax5seglem4  28916  ax5seglem5  28917  axeuclid  28947  axcontlem2  28949  axcontlem4  28951  pthdivtx  29714  spthdep  29721  usgr2wlkneq  29743  usgr2trlncl  29747  clwwlkccat  29976  clwwlkwwlksb  30040  clwwlknonel  30081  3pthdlem1  30150  uhgr3cyclexlem  30167  frgrwopreglem4a  30296  frrusgrord0lem  30325  nmlno0lem  30779  hlipgt0  30900  h1dn0  31538  spansneleq  31556  h1datomi  31567  nmlnop0iALT  31981  superpos  32340  chirredi  32380  preimane  32653  preiman0  32692  ogrpaddlt  33090  psgnfzto1stlem  33116  cycpmrn  33159  rmfsupp2  33238  pidlnzb  33442  drngidlhash  33454  constrsqrtcl  33818  qqhval2lem  34017  derangenlem  35198  subfacp1lem5  35211  btwndiff  36050  btwnconn1lem7  36116  btwnconn1lem12  36121  tan2h  37641  poimirlem1  37650  poimirlem9  37658  poimirlem17  37666  poimirlem22  37671  areacirclem1  37737  isdrngo2  37987  isdrngo3  37988  lsatn0  39022  lsatspn0  39023  lkrlspeqN  39194  cvlsupr2  39366  dalem25  39722  4atexlemcnd  40096  ltrncnvnid  40151  trlator0  40195  ltrnnidn  40198  trlnid  40203  cdleme3b  40253  cdleme11l  40293  cdleme16b  40303  cdleme35h2  40481  cdleme38n  40488  cdlemg8c  40653  cdlemg11a  40661  cdlemg12e  40671  cdlemg18a  40702  trlcoat  40747  trlcone  40752  tendo1ne0  40852  cdleml9  41008  dvheveccl  41136  dihmeetlem13N  41343  dihlspsnat  41357  dihpN  41360  dihatexv  41362  dochsat  41407  dochkrshp  41410  dochkr1  41502  lcfrlem28  41594  lcfrlem32  41598  mapdn0  41693  mapdpglem11  41706  mapdpglem16  41711  sticksstones1  42164  sn-1ne2  42283  pell1234qrne0  42851  jm2.26lem3  43000  2zrngnmlid  48210  2zrngnmrid  48211  2zrngnmlid2  48212  domnmsuppn0  48324  rmsuppss  48325  scmsuppss  48326  rrx2linest  48702  itscnhlinecirc02p  48745  inlinecirc02plem  48746  aacllem  49645