Theorem necon3d 2982

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

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

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 2962

This theorem is used by:  pssdifn0  4326  ssn0  4365  uniintsn  4955  funopsnOLD  7152  dff14i  7264  f1prex  7293  poxp3  8155  ressuppssdif  8190  suppfnss  8194  suppssov1  8202  suppssov2  8203  suppssfv  8207  omord  8562  nnmord  8627  mapdom2  9146  kmlem9  10161  isf32lem7  10361  1re  11226  addrid  11408  addn0nid  11652  nn0n0n1ge2  12590  xnegdi  13292  fseqsupubi  14034  sqrtgt0  15335  supcvg  15936  ntrivcvgfvn0  15979  efne0d  16176  efne0OLD  16178  divgcdcoprmex  16749  pceulem  16930  pcqmul  16938  pcqcl  16941  pcaddlem  16973  pcadd  16974  grpinvnz  19107  symgfvne  19482  symg2bas  19494  odmulgeq  19658  gsumval3lem2  20007  gsumval3  20008  ogrpaddlt  20239  ring1ne0  20415  ringelnzr  20658  0ringnnzr  20660  isdrng3lem2  20889  isdrng5  20891  abvdom  20970  lmodfopne  21058  mptscmfsupp0  21085  lmodindp1  21172  lspsneleq  21276  lspsneq  21283  lspexch  21290  lspindp3  21297  lspsnsubn0  21301  dsmmsubg  21930  dsmmlss  21931  elfrlmbasn0  21950  coe1tmmul2  22474  ply1scln0  22489  mavmulsolcl  22745  0ntr  23265  elcls3  23277  neindisj  23311  neindisj2  23317  conndisj  23610  dfconn2  23613  fbunfip  24063  deg1mul2  26308  ply1nzb  26317  ne0p  26401  dgreq0  26459  dgradd2  26462  dgrcolem2  26468  elqaalem3  26519  logcj  26808  argimgt0  26814  tanarg  26821  cxpsqrtth  26932  dvcnsqrt  26946  ang180lem2  27012  ftalem2  27275  ftalem4  27277  ftalem5  27278  dvdssqf  27339  cutbdaylt  28028  expsne0  28666  lmimid  29140  lmiisolem  29142  hypcgrlem1  29146  hypcgrlem2  29147  f1otrg  29257  f1otrge  29258  ax5seglem4  29319  ax5seglem5  29320  axeuclid  29350  axcontlem2  29352  axcontlem4  29354  pthdivtx  30113  spthdep  30120  usgr2wlkneq  30142  usgr2trlncl  30146  clwwlkccat  30378  clwwlkwwlksb  30442  clwwlknonel  30483  3pthdlem1  30552  uhgr3cyclexlem  30569  frgrwopreglem4a  30698  frrusgrord0lem  30727  nmlno0lem  31182  hlipgt0  31303  h1dn0  31941  spansneleq  31959  h1datomi  31970  nmlnop0iALT  32384  superpos  32743  chirredi  32783  preimane  33051  preiman0  33092  psgnfzto1stlem  33451  cycpmrn  33494  rmfsupp2  33588  pidlnzb  33761  drngidlhash  33772  extdgfialglem2  34114  constrsqrtcl  34200  qqhval2lem  34402  derangenlem  35683  subfacp1lem5  35696  btwndiff  36539  btwnconn1lem7  36605  btwnconn1lem12  36610  mh-inf3f1  37092  tan2h  38303  poimirlem1  38312  poimirlem9  38320  poimirlem17  38328  poimirlem22  38333  areacirclem1  38399  isdrngo2  38649  isdrngo3  38650  lsatn0  39813  lsatspn0  39814  lkrlspeqN  39985  cvlsupr2  40157  dalem25  40512  4atexlemcnd  40886  ltrncnvnid  40941  trlator0  40985  ltrnnidn  40988  trlnid  40993  cdleme3b  41043  cdleme11l  41083  cdleme16b  41093  cdleme35h2  41271  cdleme38n  41278  cdlemg8c  41443  cdlemg11a  41451  cdlemg12e  41461  cdlemg18a  41492  trlcoat  41537  trlcone  41542  tendo1ne0  41642  cdleml9  41798  dvheveccl  41926  dihmeetlem13N  42133  dihlspsnat  42147  dihpN  42150  dihatexv  42152  dochsat  42197  dochkrshp  42200  dochkr1  42292  lcfrlem28  42384  lcfrlem32  42388  mapdn0  42483  mapdpglem11  42496  mapdpglem16  42501  sticksstones1  42953  sn-1ne2  43072  pell1234qrne0  43620  jm2.26lem3  43768  2zrngnmlid  49060  2zrngnmrid  49061  2zrngnmlid2  49062  domnmsuppn0  49189  rmsuppss  49190  scmsuppss  49191  rrx2linest  49562  itscnhlinecirc02p  49605  inlinecirc02plem  49606  aacllem  50661