Theorem necon3d 2976

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

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

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 2956

This theorem is used by:  pssdifn0  4315  ssn0  4354  uniintsn  4944  funopsnOLD  7152  dff14i  7263  f1prex  7292  poxp3  8169  ressuppssdif  8205  suppfnss  8209  suppssov1  8217  suppssov2  8218  suppssfv  8222  omord  8579  nnmord  8644  mapdom2  9170  kmlem9  10240  isf32lem7  10440  1re  11311  addrid  11493  addn0nid  11739  nn0n0n1ge2  12677  xnegdi  13381  fseqsupubi  14124  sqrtgt0  15430  supcvg  16030  ntrivcvgfvn0  16073  efne0d  16268  efne0OLD  16270  divgcdcoprmex  16846  pceulem  17028  pcqmul  17036  pcqcl  17039  pcaddlem  17071  pcadd  17072  grpinvnz  19225  symgfvne  19600  symg2bas  19612  odmulgeq  19776  gsumval3lem2  20125  gsumval3  20126  ogrpaddlt  20357  ring1ne0  20535  ringelnzr  20779  0ringnnzr  20781  isdrng3lem2  21011  isdrng5  21013  abvdom  21092  lmodfopne  21180  mptscmfsupp0  21207  lmodindp1  21294  lspsneleq  21398  lspsneq  21405  lspexch  21412  lspindp3  21419  lspsnsubn0  21423  dsmmsubg  22054  dsmmlss  22055  elfrlmbasn0  22074  coe1tmmul2  22600  ply1scln0  22615  mavmulsolcl  22871  0ntr  23394  elcls3  23406  neindisj  23440  neindisj2  23446  conndisj  23739  dfconn2  23742  fbunfip  24193  deg1mul2  26437  ply1nzb  26446  ne0p  26530  dgreq0  26589  dgradd2  26592  dgrcolem2  26598  elqaalem3  26649  logcj  26939  argimgt0  26945  tanarg  26952  cxpsqrtth  27063  dvcnsqrt  27077  ang180lem2  27143  ftalem2  27406  ftalem4  27408  ftalem5  27409  dvdssqf  27470  cutbdaylt  28189  expsne0  28827  lmimid  29304  lmiisolem  29306  hypcgrlem1  29310  hypcgrlem2  29311  f1otrg  29453  f1otrge  29454  ax5seglem4  29515  ax5seglem5  29516  axeuclid  29546  axcontlem2  29548  axcontlem4  29550  pthdivtx  30317  spthdep  30325  usgr2wlkneq  30347  usgr2trlncl  30351  clwwlkccat  30586  clwwlkwwlksb  30650  clwwlknonel  30691  3pthdlem1  30770  uhgr3cyclexlem  30787  frgrwopreglem4a  30916  frrusgrord0lem  30945  nmlno0lem  31400  hlipgt0  31521  h1dn0  32159  spansneleq  32177  h1datomi  32188  nmlnop0iALT  32602  superpos  32961  chirredi  33001  preimane  33310  preiman0  33350  psgnfzto1stlem  33707  cycpmrn  33750  rmfsupp2  33844  pidlnzb  34018  drngidlhash  34029  extdgfialglem2  34371  constrsqrtcl  34457  qqhval2lem  34659  derangenlem  36022  subfacp1lem5  36035  btwndiff  36884  btwnconn1lem7  36950  btwnconn1lem12  36955  tan2h  38628  poimirlem1  38632  poimirlem9  38640  poimirlem17  38648  poimirlem22  38653  areacirclem1  38719  isdrngo2  38985  isdrngo3  38986  lsatn0  40149  lsatspn0  40150  lkrlspeqN  40321  cvlsupr2  40493  dalem25  40848  4atexlemcnd  41222  ltrncnvnid  41277  trlator0  41321  ltrnnidn  41324  trlnid  41329  cdleme3b  41379  cdleme11l  41419  cdleme16b  41429  cdleme35h2  41607  cdleme38n  41614  cdlemg8c  41779  cdlemg11a  41787  cdlemg12e  41797  cdlemg18a  41828  trlcoat  41873  trlcone  41878  tendo1ne0  41978  cdleml9  42134  dvheveccl  42262  dihmeetlem13N  42469  dihlspsnat  42483  dihpN  42486  dihatexv  42488  dochsat  42533  dochkrshp  42536  dochkr1  42628  lcfrlem28  42720  lcfrlem32  42724  mapdn0  42819  mapdpglem11  42832  mapdpglem16  42837  sticksstones1  43289  sn-1ne2  43423  pell1234qrne0  43953  jm2.26lem3  44101  2zrngnmlid  49445  2zrngnmrid  49446  2zrngnmlid2  49447  domnmsuppn0  49574  rmsuppss  49575  scmsuppss  49576  rrx2linest  49947  itscnhlinecirc02p  49990  inlinecirc02plem  49991  aacllem  51107