Theorem necon3d 2977

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  pssdifn0  4316  ssn0  4355  uniintsn  4945  funopsnOLD  7144  dff14i  7255  f1prex  7284  poxp3  8151  ressuppssdif  8186  suppfnss  8190  suppssov1  8198  suppssov2  8199  suppssfv  8203  omord  8560  nnmord  8625  mapdom2  9151  kmlem9  10218  isf32lem7  10418  1re  11289  addrid  11471  addn0nid  11717  nn0n0n1ge2  12655  xnegdi  13359  fseqsupubi  14101  sqrtgt0  15405  supcvg  16005  ntrivcvgfvn0  16048  efne0d  16243  efne0OLD  16245  divgcdcoprmex  16821  pceulem  17003  pcqmul  17011  pcqcl  17014  pcaddlem  17046  pcadd  17047  grpinvnz  19200  symgfvne  19575  symg2bas  19587  odmulgeq  19751  gsumval3lem2  20100  gsumval3  20101  ogrpaddlt  20332  ring1ne0  20510  ringelnzr  20754  0ringnnzr  20756  isdrng3lem2  20986  isdrng5  20988  abvdom  21067  lmodfopne  21155  mptscmfsupp0  21182  lmodindp1  21269  lspsneleq  21373  lspsneq  21380  lspexch  21387  lspindp3  21394  lspsnsubn0  21398  dsmmsubg  22029  dsmmlss  22030  elfrlmbasn0  22049  coe1tmmul2  22575  ply1scln0  22590  mavmulsolcl  22846  0ntr  23369  elcls3  23381  neindisj  23415  neindisj2  23421  conndisj  23714  dfconn2  23717  fbunfip  24168  deg1mul2  26412  ply1nzb  26421  ne0p  26505  dgreq0  26564  dgradd2  26567  dgrcolem2  26573  elqaalem3  26626  logcj  26916  argimgt0  26922  tanarg  26929  cxpsqrtth  27040  dvcnsqrt  27054  ang180lem2  27120  ftalem2  27383  ftalem4  27385  ftalem5  27386  dvdssqf  27447  cutbdaylt  28166  expsne0  28804  lmimid  29281  lmiisolem  29283  hypcgrlem1  29287  hypcgrlem2  29288  f1otrg  29430  f1otrge  29431  ax5seglem4  29492  ax5seglem5  29493  axeuclid  29523  axcontlem2  29525  axcontlem4  29527  pthdivtx  30294  spthdep  30302  usgr2wlkneq  30324  usgr2trlncl  30328  clwwlkccat  30563  clwwlkwwlksb  30627  clwwlknonel  30668  3pthdlem1  30747  uhgr3cyclexlem  30764  frgrwopreglem4a  30893  frrusgrord0lem  30922  nmlno0lem  31377  hlipgt0  31498  h1dn0  32136  spansneleq  32154  h1datomi  32165  nmlnop0iALT  32579  superpos  32938  chirredi  32978  preimane  33245  preiman0  33285  psgnfzto1stlem  33643  cycpmrn  33686  rmfsupp2  33780  pidlnzb  33954  drngidlhash  33965  extdgfialglem2  34307  constrsqrtcl  34393  qqhval2lem  34595  derangenlem  35905  subfacp1lem5  35918  btwndiff  36762  btwnconn1lem7  36828  btwnconn1lem12  36833  tan2h  38503  poimirlem1  38507  poimirlem9  38515  poimirlem17  38523  poimirlem22  38528  areacirclem1  38594  isdrngo2  38860  isdrngo3  38861  lsatn0  40024  lsatspn0  40025  lkrlspeqN  40196  cvlsupr2  40368  dalem25  40723  4atexlemcnd  41097  ltrncnvnid  41152  trlator0  41196  ltrnnidn  41199  trlnid  41204  cdleme3b  41254  cdleme11l  41294  cdleme16b  41304  cdleme35h2  41482  cdleme38n  41489  cdlemg8c  41654  cdlemg11a  41662  cdlemg12e  41672  cdlemg18a  41703  trlcoat  41748  trlcone  41753  tendo1ne0  41853  cdleml9  42009  dvheveccl  42137  dihmeetlem13N  42344  dihlspsnat  42358  dihpN  42361  dihatexv  42363  dochsat  42408  dochkrshp  42411  dochkr1  42503  lcfrlem28  42595  lcfrlem32  42599  mapdn0  42694  mapdpglem11  42707  mapdpglem16  42712  sticksstones1  43164  sn-1ne2  43298  pell1234qrne0  43813  jm2.26lem3  43961  2zrngnmlid  49296  2zrngnmrid  49297  2zrngnmlid2  49298  domnmsuppn0  49425  rmsuppss  49426  scmsuppss  49427  rrx2linest  49798  itscnhlinecirc02p  49841  inlinecirc02plem  49842  aacllem  50883