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

Theorem necon3d 2799
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 2791 . 2 (𝜑 → (𝐶𝐷 → ¬ 𝐴 = 𝐵))
3 df-ne 2778 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
42, 3syl6ibr 240 1 (𝜑 → (𝐶𝐷𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1474  wne 2776
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 195  df-ne 2778
This theorem is referenced by:  pm13.18  2859  pssdifn0  3894  ssn0  3924  uniintsn  4440  f1prex  6414  ressuppssdif  7177  suppfnss  7181  suppssov1  7188  suppssfv  7192  omord  7509  nnmord  7573  mapdom2  7990  findcard2  8059  kmlem9  8837  isf32lem7  9038  1re  9892  addid1  10064  addn0nid  10299  nn0n0n1ge2  11202  xnegdi  11904  fseqsupubi  12591  sqrtgt0  13790  supcvg  14370  ntrivcvgfvn0  14413  efne0  14609  divgcdcoprmex  15161  pceulem  15331  pcqmul  15339  pcqcl  15342  pcaddlem  15373  pcadd  15374  grpinvnz  17252  symgfvne  17574  symg2bas  17584  odmulgeq  17740  gsumval3lem2  18073  gsumval3  18074  ring1ne0  18357  abvdom  18604  lmodfopne  18667  mptscmfsupp0  18694  lmodindp1  18778  lspsneleq  18879  lspsneq  18886  lspexch  18893  lspindp3  18900  lspsnsubn0  18904  ringelnzr  19030  0ringnnzr  19033  coe1tmmul2  19410  ply1scln0  19425  dsmmsubg  19845  dsmmlss  19846  elfrlmbasn0  19864  mavmulsolcl  20115  0ntr  20624  elcls3  20636  neindisj  20670  neindisj2  20676  conndisj  20968  dfcon2  20971  fbunfip  21422  deg1mul2  23592  ply1nzb  23600  ne0p  23681  dgreq0  23739  dgradd2  23742  dgrcolem2  23748  elqaalem3  23794  logcj  24070  argimgt0  24076  tanarg  24083  dvcnsqrt  24199  ang180lem2  24254  ftalem2  24514  ftalem4  24516  ftalem5  24517  dvdssqf  24578  mirhl2  25291  lmimid  25401  lmiisolem  25403  hypcgrlem1  25406  hypcgrlem2  25407  f1otrg  25466  f1otrge  25467  ax5seglem4  25527  ax5seglem5  25528  axeuclid  25558  axcontlem2  25560  axcontlem4  25562  usgra2adedgspthlem2  25903  usgra2wlkspthlem1  25910  usgra2wlkspthlem2  25911  frgregordn0  26360  nmlno0lem  26835  hlipgt0  26957  h1dn0  27598  spansneleq  27616  h1datomi  27627  nmlnop0iALT  28041  superpos  28400  chirredi  28440  ogrpaddlt  28852  psgnfzto1stlem  28984  qqhval2lem  29156  derangenlem  30210  subfacp1lem5  30223  btwndiff  31107  btwnconn1lem7  31173  btwnconn1lem12  31178  tan2h  32371  poimirlem1  32380  poimirlem9  32388  poimirlem17  32396  poimirlem22  32401  areacirclem1  32470  isdrngo2  32727  isdrngo3  32728  lsatn0  33104  lsatspn0  33105  lkrlspeqN  33276  cvlsupr2  33448  dalem25  33802  4atexlemcnd  34176  ltrncnvnid  34231  trlator0  34276  ltrnnidn  34279  trlnid  34284  cdleme3b  34334  cdleme11l  34374  cdleme16b  34384  cdleme35h2  34563  cdleme38n  34570  cdlemg8c  34735  cdlemg11a  34743  cdlemg12e  34753  cdlemg18a  34784  trlcoat  34829  trlcone  34834  tendo1ne0  34934  cdleml9  35090  dvheveccl  35219  dihmeetlem13N  35426  dihlspsnat  35440  dihpN  35443  dihatexv  35445  dochsat  35490  dochkrshp  35493  dochkr1  35585  lcfrlem28  35677  lcfrlem32  35681  mapdn0  35776  mapdpglem11  35789  mapdpglem16  35794  pell1234qrne0  36235  jm2.26lem3  36386  funopsn  40141  pthdivtx  40934  spthdep  40939  usgr2wlkneq  40961  usgr2trlncl  40965  3pthdlem1  41330  uhgr3cyclexlem  41347  frrusgrord0  41502  2zrngnmlid  41738  2zrngnmrid  41739  2zrngnmlid2  41740  domnmsuppn0  41943  rmsuppss  41944  scmsuppss  41946  aacllem  42316
  Copyright terms: Public domain W3C validator