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

Theorem necon3d 2812
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 2804 . 2 (𝜑 → (𝐶𝐷 → ¬ 𝐴 = 𝐵))
3 df-ne 2792 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3syl6ibr 242 1 (𝜑 → (𝐶𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1481  wne 2791
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 2792
This theorem is referenced by:  pm13.18  2872  pssdifn0  3935  ssn0  3967  uniintsn  4505  funopsn  6398  f1prex  6524  ressuppssdif  7301  suppfnss  7305  suppssov1  7312  suppssfv  7316  omord  7633  nnmord  7697  mapdom2  8116  findcard2  8185  kmlem9  8965  isf32lem7  9166  1re  10024  addid1  10201  addn0nid  10436  nn0n0n1ge2  11343  xnegdi  12063  fseqsupubi  12760  sqrtgt0  13980  supcvg  14569  ntrivcvgfvn0  14612  efne0  14808  divgcdcoprmex  15361  pceulem  15531  pcqmul  15539  pcqcl  15542  pcaddlem  15573  pcadd  15574  grpinvnz  17467  symgfvne  17789  symg2bas  17799  odmulgeq  17955  gsumval3lem2  18288  gsumval3  18289  ring1ne0  18572  abvdom  18819  lmodfopne  18882  mptscmfsupp0  18909  lmodindp1  18995  lspsneleq  19096  lspsneq  19103  lspexch  19110  lspindp3  19117  lspsnsubn0  19121  ringelnzr  19247  0ringnnzr  19250  coe1tmmul2  19627  ply1scln0  19642  dsmmsubg  20068  dsmmlss  20069  elfrlmbasn0  20087  mavmulsolcl  20338  0ntr  20856  elcls3  20868  neindisj  20902  neindisj2  20908  conndisj  21200  dfconn2  21203  fbunfip  21654  deg1mul2  23855  ply1nzb  23863  ne0p  23944  dgreq0  24002  dgradd2  24005  dgrcolem2  24011  elqaalem3  24057  logcj  24333  argimgt0  24339  tanarg  24346  dvcnsqrt  24466  ang180lem2  24521  ftalem2  24781  ftalem4  24783  ftalem5  24784  dvdssqf  24845  mirhl2  25557  lmimid  25667  lmiisolem  25669  hypcgrlem1  25672  hypcgrlem2  25673  f1otrg  25732  f1otrge  25733  ax5seglem4  25793  ax5seglem5  25794  axeuclid  25824  axcontlem2  25826  axcontlem4  25828  pthdivtx  26606  spthdep  26611  usgr2wlkneq  26633  usgr2trlncl  26637  3pthdlem1  27004  uhgr3cyclexlem  27021  frrusgrord0lem  27177  nmlno0lem  27618  hlipgt0  27740  h1dn0  28381  spansneleq  28399  h1datomi  28410  nmlnop0iALT  28824  superpos  29183  chirredi  29223  ogrpaddlt  29692  psgnfzto1stlem  29824  qqhval2lem  29999  derangenlem  31127  subfacp1lem5  31140  scutbdaylt  31896  btwndiff  32109  btwnconn1lem7  32175  btwnconn1lem12  32180  tan2h  33372  poimirlem1  33381  poimirlem9  33389  poimirlem17  33397  poimirlem22  33402  areacirclem1  33471  isdrngo2  33728  isdrngo3  33729  lsatn0  34105  lsatspn0  34106  lkrlspeqN  34277  cvlsupr2  34449  dalem25  34803  4atexlemcnd  35177  ltrncnvnid  35232  trlator0  35277  ltrnnidn  35280  trlnid  35285  cdleme3b  35335  cdleme11l  35375  cdleme16b  35385  cdleme35h2  35564  cdleme38n  35571  cdlemg8c  35736  cdlemg11a  35744  cdlemg12e  35754  cdlemg18a  35785  trlcoat  35830  trlcone  35835  tendo1ne0  35935  cdleml9  36091  dvheveccl  36220  dihmeetlem13N  36427  dihlspsnat  36441  dihpN  36444  dihatexv  36446  dochsat  36491  dochkrshp  36494  dochkr1  36586  lcfrlem28  36678  lcfrlem32  36682  mapdn0  36777  mapdpglem11  36790  mapdpglem16  36795  pell1234qrne0  37236  jm2.26lem3  37387  2zrngnmlid  41714  2zrngnmrid  41715  2zrngnmlid2  41716  domnmsuppn0  41915  rmsuppss  41916  scmsuppss  41918  aacllem  42312
  Copyright terms: Public domain W3C validator