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

Theorem necon3d 2844
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 2836 . 2 (𝜑 → (𝐶𝐷 → ¬ 𝐴 = 𝐵))
3 df-ne 2824 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3syl6ibr 242 1 (𝜑 → (𝐶𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  pm13.18  2904  pssdifn0  3977  ssn0  4009  uniintsn  4546  funopsn  6453  f1prex  6579  ressuppssdif  7361  suppfnss  7365  suppssov1  7372  suppssfv  7376  omord  7693  nnmord  7757  mapdom2  8172  findcard2  8241  kmlem9  9018  isf32lem7  9219  1re  10077  addid1  10254  addn0nid  10489  nn0n0n1ge2  11396  xnegdi  12116  fseqsupubi  12817  sqrtgt0  14043  supcvg  14632  ntrivcvgfvn0  14675  efne0  14871  divgcdcoprmex  15427  pceulem  15597  pcqmul  15605  pcqcl  15608  pcaddlem  15639  pcadd  15640  grpinvnz  17533  symgfvne  17854  symg2bas  17864  odmulgeq  18020  gsumval3lem2  18353  gsumval3  18354  ring1ne0  18637  abvdom  18886  lmodfopne  18949  mptscmfsupp0  18976  lmodindp1  19062  lspsneleq  19163  lspsneq  19170  lspexch  19177  lspindp3  19184  lspsnsubn0  19188  ringelnzr  19314  0ringnnzr  19317  coe1tmmul2  19694  ply1scln0  19709  dsmmsubg  20135  dsmmlss  20136  elfrlmbasn0  20154  mavmulsolcl  20405  0ntr  20923  elcls3  20935  neindisj  20969  neindisj2  20975  conndisj  21267  dfconn2  21270  fbunfip  21720  deg1mul2  23919  ply1nzb  23927  ne0p  24008  dgreq0  24066  dgradd2  24069  dgrcolem2  24075  elqaalem3  24121  logcj  24397  argimgt0  24403  tanarg  24410  dvcnsqrt  24530  ang180lem2  24585  ftalem2  24845  ftalem4  24847  ftalem5  24848  dvdssqf  24909  mirhl2  25621  lmimid  25731  lmiisolem  25733  hypcgrlem1  25736  hypcgrlem2  25737  f1otrg  25796  f1otrge  25797  ax5seglem4  25857  ax5seglem5  25858  axeuclid  25888  axcontlem2  25890  axcontlem4  25892  pthdivtx  26681  spthdep  26686  usgr2wlkneq  26708  usgr2trlncl  26712  clwwlkwwlksb  27018  clwwlknonel  27070  3pthdlem1  27142  uhgr3cyclexlem  27159  frgrwopreglem4a  27290  frrusgrord0lem  27319  clwwlkccat  27332  nmlno0lem  27776  hlipgt0  27898  h1dn0  28539  spansneleq  28557  h1datomi  28568  nmlnop0iALT  28982  superpos  29341  chirredi  29381  ogrpaddlt  29846  psgnfzto1stlem  29978  qqhval2lem  30153  derangenlem  31279  subfacp1lem5  31292  scutbdaylt  32047  btwndiff  32259  btwnconn1lem7  32325  btwnconn1lem12  32330  tan2h  33531  poimirlem1  33540  poimirlem9  33548  poimirlem17  33556  poimirlem22  33561  areacirclem1  33630  isdrngo2  33887  isdrngo3  33888  lsatn0  34604  lsatspn0  34605  lkrlspeqN  34776  cvlsupr2  34948  dalem25  35302  4atexlemcnd  35676  ltrncnvnid  35731  trlator0  35776  ltrnnidn  35779  trlnid  35784  cdleme3b  35834  cdleme11l  35874  cdleme16b  35884  cdleme35h2  36062  cdleme38n  36069  cdlemg8c  36234  cdlemg11a  36242  cdlemg12e  36252  cdlemg18a  36283  trlcoat  36328  trlcone  36333  tendo1ne0  36433  cdleml9  36589  dvheveccl  36718  dihmeetlem13N  36925  dihlspsnat  36939  dihpN  36942  dihatexv  36944  dochsat  36989  dochkrshp  36992  dochkr1  37084  lcfrlem28  37176  lcfrlem32  37180  mapdn0  37275  mapdpglem11  37288  mapdpglem16  37293  pell1234qrne0  37734  jm2.26lem3  37885  2zrngnmlid  42274  2zrngnmrid  42275  2zrngnmlid2  42276  domnmsuppn0  42475  rmsuppss  42476  scmsuppss  42478  aacllem  42875
  Copyright terms: Public domain W3C validator