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

Theorem necon3d 2497
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 2495 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 218 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon3i  2498  pm13.18  2531  ssn0  3500  pssdifn0  3528  uniintsn  3915  suppssfv  6090  suppssov1  6091  omord  6582  nnmord  6646  mapdom2  7048  findcard2  7114  kmlem9  7800  isf32lem7  8001  1re  8853  addid1  9008  xnegdi  10584  fseqsupubi  11056  sqrgt0  11760  supcvg  12330  efne0  12393  pceulem  12914  pcqmul  12922  pcqcl  12925  pcaddlem  12952  pcadd  12953  grpinvnz  14555  odmulgeq  14886  gsumval3  15207  abvdom  15619  lmodindp1  15787  lspsneleq  15884  lspsneq  15891  lspexch  15898  lspindp3  15905  lspsnsubn0  15909  rngelnzr  16033  coe1tmmul2  16368  ply1scln0  16382  0ntr  16824  elcls3  16836  neindisj  16870  neindisj2  16876  conndisj  17158  dfcon2  17161  fbunfip  17580  deg1mul2  19516  ply1nzb  19524  ne0p  19605  dgreq0  19662  dgradd2  19665  dgrcolem2  19671  elqaalem3  19717  logcj  19976  argimgt0  19982  tanarg  19986  ang180lem2  20124  ftalem2  20327  ftalem4  20329  ftalem5  20330  dvdssqf  20392  nmlno0lem  21387  hlipgt0  21509  h1dn0  22147  spansneleq  22165  h1datomi  22176  nmlnop0iALT  22591  superpos  22950  chirredi  22990  derangenlem  23717  subfacp1lem5  23730  ax5seglem4  24632  ax5seglem5  24633  axeuclid  24663  axcontlem2  24665  axcontlem4  24667  btwndiff  24722  btwnconn1lem7  24788  btwnconn1lem12  24793  dvreacos  25027  areacirclem2  25028  hdrmp  25809  isdrngo2  26692  isdrngo3  26693  pell1234qrne0  27041  jm2.26lem3  27197  dsmmsubg  27312  dsmmlss  27313  lsatn0  29811  lsatspn0  29812  lkrlspeqN  29983  cvlsupr2  30155  dalem25  30509  4atexlemcnd  30883  ltrncnvnid  30938  trlator0  30982  ltrnnidn  30985  trlnid  30990  cdleme3b  31040  cdleme11l  31080  cdleme16b  31090  cdleme35h2  31268  cdleme38n  31275  cdlemg8c  31440  cdlemg11a  31448  cdlemg12e  31458  cdlemg18a  31489  trlcoat  31534  trlcone  31539  tendo1ne0  31639  cdleml9  31795  dvheveccl  31924  dihmeetlem13N  32131  dihlspsnat  32145  dihpN  32148  dihatexv  32150  dochsat  32195  dochkrshp  32198  dochkr1  32290  lcfrlem28  32382  lcfrlem32  32386  mapdn0  32481  mapdpglem11  32494  mapdpglem16  32499
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2461
  Copyright terms: Public domain W3C validator