MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3d Structured version   Visualization version   GIF version

Theorem necon3d 2958
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
StepHypRef Expression
1 necon3d.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
21necon3ad 2950 . 2 (𝜑 → (𝐶𝐷 → ¬ 𝐴 = 𝐵))
3 df-ne 2938 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3syl6ibr 243 1 (𝜑 → (𝐶𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1652  wne 2937
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 198  df-ne 2938
This theorem is referenced by:  pm13.18  3018  pssdifn0  4108  ssn0  4138  uniintsn  4670  funopsn  6605  f1prex  6731  ressuppssdif  7518  suppfnss  7522  suppfnssOLD  7523  suppssov1  7530  suppssfv  7534  omord  7853  nnmord  7917  mapdom2  8338  findcard2  8407  kmlem9  9233  isf32lem7  9434  1re  10293  addid1  10470  addn0nid  10705  nn0n0n1ge2  11605  xnegdi  12280  fseqsupubi  12985  sqrtgt0  14284  supcvg  14872  ntrivcvgfvn0  14914  efne0  15109  divgcdcoprmex  15660  pceulem  15829  pcqmul  15837  pcqcl  15840  pcaddlem  15871  pcadd  15872  grpinvnz  17753  symgfvne  18071  symg2bas  18081  odmulgeq  18238  gsumval3lem2  18573  gsumval3  18574  ring1ne0  18858  abvdom  19107  lmodfopne  19170  mptscmfsupp0  19197  lmodindp1  19286  lspsneleq  19387  lspsneq  19394  lspexch  19402  lspindp3  19409  lspsnsubn0  19413  ringelnzr  19540  0ringnnzr  19543  coe1tmmul2  19919  ply1scln0  19934  dsmmsubg  20363  dsmmlss  20364  elfrlmbasn0  20382  mavmulsolcl  20634  0ntr  21155  elcls3  21167  neindisj  21201  neindisj2  21207  conndisj  21499  dfconn2  21502  fbunfip  21952  deg1mul2  24165  ply1nzb  24173  ne0p  24254  dgreq0  24312  dgradd2  24315  dgrcolem2  24321  elqaalem3  24367  logcj  24643  argimgt0  24649  tanarg  24656  dvcnsqrt  24776  ang180lem2  24831  ftalem2  25091  ftalem4  25093  ftalem5  25094  dvdssqf  25155  mirhl2  25867  lmimid  25977  lmiisolem  25979  hypcgrlem1  25982  hypcgrlem2  25983  f1otrg  26042  f1otrge  26043  ax5seglem4  26103  ax5seglem5  26104  axeuclid  26134  axcontlem2  26136  axcontlem4  26138  pthdivtx  26917  spthdep  26922  usgr2wlkneq  26944  usgr2trlncl  26948  clwwlkccat  27217  clwwlkwwlksb  27304  clwwlknonel  27367  3pthdlem1  27442  uhgr3cyclexlem  27459  frgrwopreglem4a  27590  frrusgrord0lem  27619  nmlno0lem  28104  hlipgt0  28226  h1dn0  28867  spansneleq  28885  h1datomi  28896  nmlnop0iALT  29310  superpos  29669  chirredi  29709  ogrpaddlt  30165  psgnfzto1stlem  30297  qqhval2lem  30472  derangenlem  31601  subfacp1lem5  31614  scutbdaylt  32366  btwndiff  32578  btwnconn1lem7  32644  btwnconn1lem12  32649  tan2h  33825  poimirlem1  33834  poimirlem9  33842  poimirlem17  33850  poimirlem22  33855  areacirclem1  33923  isdrngo2  34179  isdrngo3  34180  lsatn0  34955  lsatspn0  34956  lkrlspeqN  35127  cvlsupr2  35299  dalem25  35654  4atexlemcnd  36028  ltrncnvnid  36083  trlator0  36127  ltrnnidn  36130  trlnid  36135  cdleme3b  36185  cdleme11l  36225  cdleme16b  36235  cdleme35h2  36413  cdleme38n  36420  cdlemg8c  36585  cdlemg11a  36593  cdlemg12e  36603  cdlemg18a  36634  trlcoat  36679  trlcone  36684  tendo1ne0  36784  cdleml9  36940  dvheveccl  37068  dihmeetlem13N  37275  dihlspsnat  37289  dihpN  37292  dihatexv  37294  dochsat  37339  dochkrshp  37342  dochkr1  37434  lcfrlem28  37526  lcfrlem32  37530  mapdn0  37625  mapdpglem11  37638  mapdpglem16  37643  pell1234qrne0  38095  jm2.26lem3  38245  2zrngnmlid  42618  2zrngnmrid  42619  2zrngnmlid2  42620  domnmsuppn0  42819  rmsuppss  42820  scmsuppss  42822  aacllem  43219
  Copyright terms: Public domain W3C validator