Theorem necon3d 2961

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

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

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 2941

This theorem is referenced by:  pssdifn0  4368  ssn0  4404  uniintsn  4985  funopsn  7168  f1prex  7304  poxp3  8175  ressuppssdif  8210  suppfnss  8214  suppssov1  8222  suppssov2  8223  suppssfv  8227  omord  8606  nnmord  8670  mapdom2  9188  kmlem9  10199  isf32lem7  10399  1re  11261  addrid  11441  addn0nid  11683  nn0n0n1ge2  12594  xnegdi  13290  fseqsupubi  14019  sqrtgt0  15297  supcvg  15892  ntrivcvgfvn0  15935  efne0  16133  divgcdcoprmex  16703  pceulem  16883  pcqmul  16891  pcqcl  16894  pcaddlem  16926  pcadd  16927  grpinvnz  19028  symgfvne  19398  symg2bas  19410  odmulgeq  19575  gsumval3lem2  19924  gsumval3  19925  ring1ne0  20296  ringelnzr  20523  0ringnnzr  20525  abvdom  20831  lmodfopne  20898  mptscmfsupp0  20925  lmodindp1  21012  lspsneleq  21117  lspsneq  21124  lspexch  21131  lspindp3  21138  lspsnsubn0  21142  dsmmsubg  21763  dsmmlss  21764  elfrlmbasn0  21783  coe1tmmul2  22279  ply1scln0  22295  mavmulsolcl  22557  0ntr  23079  elcls3  23091  neindisj  23125  neindisj2  23131  conndisj  23424  dfconn2  23427  fbunfip  23877  deg1mul2  26153  ply1nzb  26162  ne0p  26246  dgreq0  26305  dgradd2  26308  dgrcolem2  26314  elqaalem3  26363  logcj  26648  argimgt0  26654  tanarg  26661  cxpsqrtth  26772  dvcnsqrt  26786  ang180lem2  26853  ftalem2  27117  ftalem4  27119  ftalem5  27120  dvdssqf  27181  scutbdaylt  27863  expsne0  28414  lmimid  28802  lmiisolem  28804  hypcgrlem1  28807  hypcgrlem2  28808  f1otrg  28879  f1otrge  28880  ax5seglem4  28947  ax5seglem5  28948  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  pthdivtx  29747  spthdep  29754  usgr2wlkneq  29776  usgr2trlncl  29780  clwwlkccat  30009  clwwlkwwlksb  30073  clwwlknonel  30114  3pthdlem1  30183  uhgr3cyclexlem  30200  frgrwopreglem4a  30329  frrusgrord0lem  30358  nmlno0lem  30812  hlipgt0  30933  h1dn0  31571  spansneleq  31589  h1datomi  31600  nmlnop0iALT  32014  superpos  32373  chirredi  32413  preimane  32680  preiman0  32719  ogrpaddlt  33094  psgnfzto1stlem  33120  cycpmrn  33163  rmfsupp2  33242  pidlnzb  33450  drngidlhash  33462  qqhval2lem  33982  derangenlem  35176  subfacp1lem5  35189  btwndiff  36028  btwnconn1lem7  36094  btwnconn1lem12  36099  tan2h  37619  poimirlem1  37628  poimirlem9  37636  poimirlem17  37644  poimirlem22  37649  areacirclem1  37715  isdrngo2  37965  isdrngo3  37966  lsatn0  39000  lsatspn0  39001  lkrlspeqN  39172  cvlsupr2  39344  dalem25  39700  4atexlemcnd  40074  ltrncnvnid  40129  trlator0  40173  ltrnnidn  40176  trlnid  40181  cdleme3b  40231  cdleme11l  40271  cdleme16b  40281  cdleme35h2  40459  cdleme38n  40466  cdlemg8c  40631  cdlemg11a  40639  cdlemg12e  40649  cdlemg18a  40680  trlcoat  40725  trlcone  40730  tendo1ne0  40830  cdleml9  40986  dvheveccl  41114  dihmeetlem13N  41321  dihlspsnat  41335  dihpN  41338  dihatexv  41340  dochsat  41385  dochkrshp  41388  dochkr1  41480  lcfrlem28  41572  lcfrlem32  41576  mapdn0  41671  mapdpglem11  41684  mapdpglem16  41689  sticksstones1  42147  sn-1ne2  42300  efne0d  42373  pell1234qrne0  42864  jm2.26lem3  43013  2zrngnmlid  48171  2zrngnmrid  48172  2zrngnmlid2  48173  domnmsuppn0  48285  rmsuppss  48286  scmsuppss  48287  rrx2linest  48663  itscnhlinecirc02p  48706  inlinecirc02plem  48707  aacllem  49320