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

Theorem necon3d 2636
Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
Hypothesis
Ref Expression
necon3d.1  |-  ( ph  ->  ( A  =  B  ->  C  =  D ) )
Assertion
Ref Expression
necon3d  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )

Proof of Theorem necon3d
StepHypRef Expression
1 necon3d.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  C  =  D ) )
21necon3ad 2634 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2598 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 227 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1362    =/= wne 2596
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 185  df-ne 2598
This theorem is referenced by:  necon3i  2640  pm13.18  2673  ssn0  3658  pssdifn0  3728  uniintsn  4153  suppssfvOLD  6305  suppssov1OLD  6306  ressuppssdif  6699  suppfnss  6703  suppssov1  6710  suppssfv  6714  omord  6995  nnmord  7059  mapdom2  7470  findcard2  7540  kmlem9  8315  isf32lem7  8516  1re  9373  addid1  9537  nn0n0n1ge2  10631  xnegdi  11199  fseqsupubi  11784  sqrgt0  12732  supcvg  13301  efne0  13364  pceulem  13895  pcqmul  13903  pcqcl  13906  pcaddlem  13933  pcadd  13934  grpinvnz  15577  symgfvne  15873  symg2bas  15883  odmulgeq  16038  gsumval3OLD  16362  gsumval3lem2  16364  gsumval3  16365  abvdom  16847  lmodindp1  17017  lspsneleq  17118  lspsneq  17125  lspexch  17132  lspindp3  17139  lspsnsubn0  17143  rngelnzr  17269  coe1tmmul2  17627  ply1scln0  17641  dsmmsubg  18010  dsmmlss  18011  elfrlmbasn0  18032  mavmulsolcl  18204  0ntr  18517  elcls3  18529  neindisj  18563  neindisj2  18569  conndisj  18862  dfcon2  18865  fbunfip  19284  deg1mul2  21471  ply1nzb  21479  ne0p  21560  dgreq0  21617  dgradd2  21620  dgrcolem2  21626  elqaalem3  21672  logcj  21940  argimgt0  21946  tanarg  21953  ang180lem2  22091  ftalem2  22296  ftalem4  22298  ftalem5  22299  dvdssqf  22361  f1otrg  22940  f1otrge  22941  ax5seglem4  23001  ax5seglem5  23002  axeuclid  23032  axcontlem2  23034  axcontlem4  23036  nmlno0lem  24016  hlipgt0  24138  h1dn0  24778  spansneleq  24796  h1datomi  24807  nmlnop0iALT  25222  superpos  25581  chirredi  25621  ogrpaddlt  26005  qqhval2lem  26264  derangenlem  26907  subfacp1lem5  26920  ntrivcvgfvn0  27261  btwndiff  27905  btwnconn1lem7  27971  btwnconn1lem12  27976  tan2h  28268  dvcnsqr  28322  areacirclem1  28328  isdrngo2  28608  isdrngo3  28609  pell1234qrne0  29039  jm2.26lem3  29195  usgra2wlkspthlem1  30142  usgra2wlkspthlem2  30143  usgra2adedgspthlem2  30150  frgregordn0  30509  rng1ne0  30604  0rngnnzr  30609  domnmsuppn0  30613  rmsuppss  30614  scmsuppss  30616  lsatn0  32217  lsatspn0  32218  lkrlspeqN  32389  cvlsupr2  32561  dalem25  32915  4atexlemcnd  33289  ltrncnvnid  33344  trlator0  33388  ltrnnidn  33391  trlnid  33396  cdleme3b  33446  cdleme11l  33486  cdleme16b  33496  cdleme35h2  33674  cdleme38n  33681  cdlemg8c  33846  cdlemg11a  33854  cdlemg12e  33864  cdlemg18a  33895  trlcoat  33940  trlcone  33945  tendo1ne0  34045  cdleml9  34201  dvheveccl  34330  dihmeetlem13N  34537  dihlspsnat  34551  dihpN  34554  dihatexv  34556  dochsat  34601  dochkrshp  34604  dochkr1  34696  lcfrlem28  34788  lcfrlem32  34792  mapdn0  34887  mapdpglem11  34900  mapdpglem16  34905
  Copyright terms: Public domain W3C validator