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	syl6ibr 251	1 ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ 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 206  df-ne 2941

This theorem is referenced by:  pssdifn0  4364  ssn0  4399  uniintsn  4990  funopsn  7142  f1prex  7278  poxp3  8132  ressuppssdif  8166  suppfnss  8170  suppssov1  8179  suppssfv  8183  omord  8564  nnmord  8628  mapdom2  9144  findcard2OLD  9280  kmlem9  10149  isf32lem7  10350  1re  11210  addrid  11390  addn0nid  11630  nn0n0n1ge2  12535  xnegdi  13223  fseqsupubi  13939  sqrtgt0  15201  supcvg  15798  ntrivcvgfvn0  15841  efne0  16036  divgcdcoprmex  16599  pceulem  16774  pcqmul  16782  pcqcl  16785  pcaddlem  16817  pcadd  16818  grpinvnz  18890  symgfvne  19242  symg2bas  19254  odmulgeq  19419  gsumval3lem2  19768  gsumval3  19769  ring1ne0  20104  ringelnzr  20292  0ringnnzr  20294  abvdom  20438  lmodfopne  20502  mptscmfsupp0  20529  lmodindp1  20617  lspsneleq  20720  lspsneq  20727  lspexch  20734  lspindp3  20741  lspsnsubn0  20745  dsmmsubg  21289  dsmmlss  21290  elfrlmbasn0  21309  coe1tmmul2  21789  ply1scln0  21805  mavmulsolcl  22044  0ntr  22566  elcls3  22578  neindisj  22612  neindisj2  22618  conndisj  22911  dfconn2  22914  fbunfip  23364  deg1mul2  25623  ply1nzb  25631  ne0p  25712  dgreq0  25770  dgradd2  25773  dgrcolem2  25779  elqaalem3  25825  logcj  26105  argimgt0  26111  tanarg  26118  cxpsqrtth  26228  dvcnsqrt  26241  ang180lem2  26304  ftalem2  26567  ftalem4  26569  ftalem5  26570  dvdssqf  26631  scutbdaylt  27308  lmimid  28034  lmiisolem  28036  hypcgrlem1  28039  hypcgrlem2  28040  f1otrg  28111  f1otrge  28112  ax5seglem4  28179  ax5seglem5  28180  axeuclid  28210  axcontlem2  28212  axcontlem4  28214  pthdivtx  28975  spthdep  28980  usgr2wlkneq  29002  usgr2trlncl  29006  clwwlkccat  29232  clwwlkwwlksb  29296  clwwlknonel  29337  3pthdlem1  29406  uhgr3cyclexlem  29423  frgrwopreglem4a  29552  frrusgrord0lem  29581  nmlno0lem  30033  hlipgt0  30154  h1dn0  30792  spansneleq  30810  h1datomi  30821  nmlnop0iALT  31235  superpos  31594  chirredi  31634  preimane  31882  preiman0  31918  ogrpaddlt  32222  psgnfzto1stlem  32246  cycpmrn  32289  rmfsupp2  32375  pidlnzb  32528  drngidlhash  32540  qqhval2lem  32949  derangenlem  34150  subfacp1lem5  34163  btwndiff  34987  btwnconn1lem7  35053  btwnconn1lem12  35058  tan2h  36468  poimirlem1  36477  poimirlem9  36485  poimirlem17  36493  poimirlem22  36498  areacirclem1  36564  isdrngo2  36814  isdrngo3  36815  lsatn0  37857  lsatspn0  37858  lkrlspeqN  38029  cvlsupr2  38201  dalem25  38557  4atexlemcnd  38931  ltrncnvnid  38986  trlator0  39030  ltrnnidn  39033  trlnid  39038  cdleme3b  39088  cdleme11l  39128  cdleme16b  39138  cdleme35h2  39316  cdleme38n  39323  cdlemg8c  39488  cdlemg11a  39496  cdlemg12e  39506  cdlemg18a  39537  trlcoat  39582  trlcone  39587  tendo1ne0  39687  cdleml9  39843  dvheveccl  39971  dihmeetlem13N  40178  dihlspsnat  40192  dihpN  40195  dihatexv  40197  dochsat  40242  dochkrshp  40245  dochkr1  40337  lcfrlem28  40429  lcfrlem32  40433  mapdn0  40528  mapdpglem11  40541  mapdpglem16  40546  sticksstones1  40950  sn-1ne2  41176  pell1234qrne0  41576  jm2.26lem3  41725  2zrngnmlid  46800  2zrngnmrid  46801  2zrngnmlid2  46802  domnmsuppn0  46998  rmsuppss  46999  scmsuppss  47001  rrx2linest  47381  itscnhlinecirc02p  47424  inlinecirc02plem  47425  aacllem  47801