Theorem necon3d 2953

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

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

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 2933

This theorem is referenced by:  pssdifn0  4308  ssn0  4344  uniintsn  4927  funopsnOLD  7102  dff14i  7214  f1prex  7239  poxp3  8100  ressuppssdif  8135  suppfnss  8139  suppssov1  8147  suppssov2  8148  suppssfv  8152  omord  8503  nnmord  8568  mapdom2  9086  kmlem9  10081  isf32lem7  10281  1re  11144  addrid  11326  addn0nid  11570  nn0n0n1ge2  12505  xnegdi  13200  fseqsupubi  13940  sqrtgt0  15220  supcvg  15821  ntrivcvgfvn0  15864  efne0d  16062  efne0OLD  16064  divgcdcoprmex  16635  pceulem  16816  pcqmul  16824  pcqcl  16827  pcaddlem  16859  pcadd  16860  grpinvnz  18986  symgfvne  19356  symg2bas  19368  odmulgeq  19532  gsumval3lem2  19881  gsumval3  19882  ogrpaddlt  20113  ring1ne0  20280  ringelnzr  20500  0ringnnzr  20502  abvdom  20807  lmodfopne  20895  mptscmfsupp0  20922  lmodindp1  21009  lspsneleq  21113  lspsneq  21120  lspexch  21127  lspindp3  21134  lspsnsubn0  21138  dsmmsubg  21723  dsmmlss  21724  elfrlmbasn0  21743  coe1tmmul2  22241  ply1scln0  22256  mavmulsolcl  22516  0ntr  23036  elcls3  23048  neindisj  23082  neindisj2  23088  conndisj  23381  dfconn2  23384  fbunfip  23834  deg1mul2  26079  ply1nzb  26088  ne0p  26172  dgreq0  26230  dgradd2  26233  dgrcolem2  26239  elqaalem3  26287  logcj  26570  argimgt0  26576  tanarg  26583  cxpsqrtth  26694  dvcnsqrt  26708  ang180lem2  26774  ftalem2  27037  ftalem4  27039  ftalem5  27040  dvdssqf  27101  cutbdaylt  27790  expsne0  28428  lmimid  28862  lmiisolem  28864  hypcgrlem1  28867  hypcgrlem2  28868  f1otrg  28939  f1otrge  28940  ax5seglem4  29001  ax5seglem5  29002  axeuclid  29032  axcontlem2  29034  axcontlem4  29036  pthdivtx  29795  spthdep  29802  usgr2wlkneq  29824  usgr2trlncl  29828  clwwlkccat  30060  clwwlkwwlksb  30124  clwwlknonel  30165  3pthdlem1  30234  uhgr3cyclexlem  30251  frgrwopreglem4a  30380  frrusgrord0lem  30409  nmlno0lem  30864  hlipgt0  30985  h1dn0  31623  spansneleq  31641  h1datomi  31652  nmlnop0iALT  32066  superpos  32425  chirredi  32465  preimane  32742  preiman0  32783  psgnfzto1stlem  33161  cycpmrn  33204  rmfsupp2  33299  pidlnzb  33482  drngidlhash  33494  extdgfialglem2  33837  constrsqrtcl  33923  qqhval2lem  34125  derangenlem  35353  subfacp1lem5  35366  btwndiff  36209  btwnconn1lem7  36275  btwnconn1lem12  36280  mh-inf3f1  36723  tan2h  37933  poimirlem1  37942  poimirlem9  37950  poimirlem17  37958  poimirlem22  37963  areacirclem1  38029  isdrngo2  38279  isdrngo3  38280  lsatn0  39445  lsatspn0  39446  lkrlspeqN  39617  cvlsupr2  39789  dalem25  40144  4atexlemcnd  40518  ltrncnvnid  40573  trlator0  40617  ltrnnidn  40620  trlnid  40625  cdleme3b  40675  cdleme11l  40715  cdleme16b  40725  cdleme35h2  40903  cdleme38n  40910  cdlemg8c  41075  cdlemg11a  41083  cdlemg12e  41093  cdlemg18a  41124  trlcoat  41169  trlcone  41174  tendo1ne0  41274  cdleml9  41430  dvheveccl  41558  dihmeetlem13N  41765  dihlspsnat  41779  dihpN  41782  dihatexv  41784  dochsat  41829  dochkrshp  41832  dochkr1  41924  lcfrlem28  42016  lcfrlem32  42020  mapdn0  42115  mapdpglem11  42128  mapdpglem16  42133  sticksstones1  42585  sn-1ne2  42703  pell1234qrne0  43281  jm2.26lem3  43429  2zrngnmlid  48731  2zrngnmrid  48732  2zrngnmlid2  48733  domnmsuppn0  48845  rmsuppss  48846  scmsuppss  48847  rrx2linest  49218  itscnhlinecirc02p  49261  inlinecirc02plem  49262  aacllem  50276