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

Theorem necon3d 3011
 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 3003 . 2 (𝜑 → (𝐶𝐷 → ¬ 𝐴 = 𝐵))
3 df-ne 2991 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3syl6ibr 255 1 (𝜑 → (𝐶𝐷𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2990 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 210  df-ne 2991 This theorem is referenced by:  pssdifn0  4282  ssn0  4311  uniintsn  4878  funopsn  6891  f1prex  7022  ressuppssdif  7838  suppfnss  7842  suppssov1  7849  suppssfv  7853  omord  8181  nnmord  8245  mapdom2  8676  findcard2  8746  kmlem9  9573  isf32lem7  9774  1re  10634  addid1  10813  addn0nid  11053  nn0n0n1ge2  11954  xnegdi  12633  fseqsupubi  13345  sqrtgt0  14613  supcvg  15206  ntrivcvgfvn0  15250  efne0  15445  divgcdcoprmex  16003  pceulem  16175  pcqmul  16183  pcqcl  16186  pcaddlem  16217  pcadd  16218  grpinvnz  18165  symgfvne  18504  symg2bas  18516  odmulgeq  18679  gsumval3lem2  19022  gsumval3  19023  ring1ne0  19340  abvdom  19605  lmodfopne  19668  mptscmfsupp0  19695  lmodindp1  19782  lspsneleq  19883  lspsneq  19890  lspexch  19897  lspindp3  19904  lspsnsubn0  19908  ringelnzr  20035  0ringnnzr  20038  dsmmsubg  20435  dsmmlss  20436  elfrlmbasn0  20455  coe1tmmul2  20908  ply1scln0  20923  mavmulsolcl  21159  0ntr  21679  elcls3  21691  neindisj  21725  neindisj2  21731  conndisj  22024  dfconn2  22027  fbunfip  22477  deg1mul2  24718  ply1nzb  24726  ne0p  24807  dgreq0  24865  dgradd2  24868  dgrcolem2  24874  elqaalem3  24920  logcj  25200  argimgt0  25206  tanarg  25213  cxpsqrtth  25323  dvcnsqrt  25336  ang180lem2  25399  ftalem2  25662  ftalem4  25664  ftalem5  25665  dvdssqf  25726  lmimid  26591  lmiisolem  26593  hypcgrlem1  26596  hypcgrlem2  26597  f1otrg  26668  f1otrge  26669  ax5seglem4  26729  ax5seglem5  26730  axeuclid  26760  axcontlem2  26762  axcontlem4  26764  pthdivtx  27521  spthdep  27526  usgr2wlkneq  27548  usgr2trlncl  27552  clwwlkccat  27778  clwwlkwwlksb  27842  clwwlknonel  27883  3pthdlem1  27952  uhgr3cyclexlem  27969  frgrwopreglem4a  28098  frrusgrord0lem  28127  nmlno0lem  28579  hlipgt0  28700  h1dn0  29338  spansneleq  29356  h1datomi  29367  nmlnop0iALT  29781  superpos  30140  chirredi  30180  preimane  30436  preiman0  30472  ogrpaddlt  30771  psgnfzto1stlem  30795  cycpmrn  30838  rmfsupp2  30920  qqhval2lem  31330  derangenlem  32526  subfacp1lem5  32539  scutbdaylt  33384  btwndiff  33596  btwnconn1lem7  33662  btwnconn1lem12  33667  tan2h  35042  poimirlem1  35051  poimirlem9  35059  poimirlem17  35067  poimirlem22  35072  areacirclem1  35138  isdrngo2  35389  isdrngo3  35390  lsatn0  36288  lsatspn0  36289  lkrlspeqN  36460  cvlsupr2  36632  dalem25  36987  4atexlemcnd  37361  ltrncnvnid  37416  trlator0  37460  ltrnnidn  37463  trlnid  37468  cdleme3b  37518  cdleme11l  37558  cdleme16b  37568  cdleme35h2  37746  cdleme38n  37753  cdlemg8c  37918  cdlemg11a  37926  cdlemg12e  37936  cdlemg18a  37967  trlcoat  38012  trlcone  38017  tendo1ne0  38117  cdleml9  38273  dvheveccl  38401  dihmeetlem13N  38608  dihlspsnat  38622  dihpN  38625  dihatexv  38627  dochsat  38672  dochkrshp  38675  dochkr1  38767  lcfrlem28  38859  lcfrlem32  38863  mapdn0  38958  mapdpglem11  38971  mapdpglem16  38976  sn-1ne2  39453  pell1234qrne0  39781  jm2.26lem3  39929  2zrngnmlid  44560  2zrngnmrid  44561  2zrngnmlid2  44562  domnmsuppn0  44758  rmsuppss  44759  scmsuppss  44761  rrx2linest  45143  itscnhlinecirc02p  45186  inlinecirc02plem  45187  aacllem  45316
 Copyright terms: Public domain W3C validator