MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3d 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 2600 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 219 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon3i  2637  pm13.18  2670  ssn0  3652  pssdifn0  3681  uniintsn  4079  suppssfv  6292  suppssov1  6293  omord  6802  nnmord  6866  mapdom2  7269  findcard2  7339  kmlem9  8027  isf32lem7  8228  1re  9079  addid1  9235  nn0n0n1ge2  10269  xnegdi  10816  fseqsupubi  11305  sqrgt0  12052  supcvg  12623  efne0  12686  pceulem  13207  pcqmul  13215  pcqcl  13218  pcaddlem  13245  pcadd  13246  grpinvnz  14850  odmulgeq  15181  gsumval3  15502  abvdom  15914  lmodindp1  16078  lspsneleq  16175  lspsneq  16182  lspexch  16189  lspindp3  16196  lspsnsubn0  16200  rngelnzr  16324  coe1tmmul2  16656  ply1scln0  16670  0ntr  17123  elcls3  17135  neindisj  17169  neindisj2  17175  conndisj  17467  dfcon2  17470  fbunfip  17889  deg1mul2  20025  ply1nzb  20033  ne0p  20114  dgreq0  20171  dgradd2  20174  dgrcolem2  20180  elqaalem3  20226  logcj  20489  argimgt0  20495  tanarg  20502  ang180lem2  20640  ftalem2  20844  ftalem4  20846  ftalem5  20847  dvdssqf  20909  nmlno0lem  22282  hlipgt0  22404  h1dn0  23042  spansneleq  23060  h1datomi  23071  nmlnop0iALT  23486  superpos  23845  chirredi  23885  ofldaddlt  24229  qqhval2lem  24353  derangenlem  24845  subfacp1lem5  24858  ntrivcvgfvn0  25216  ax5seglem4  25819  ax5seglem5  25820  axeuclid  25850  axcontlem2  25852  axcontlem4  25854  btwndiff  25909  btwnconn1lem7  25975  btwnconn1lem12  25980  dvreacos  26227  areacirclem2  26228  isdrngo2  26511  isdrngo3  26512  pell1234qrne0  26853  jm2.26lem3  27009  dsmmsubg  27124  dsmmlss  27125  usgra2wlkspthlem1  28180  usgra2wlkspthlem2  28181  usgra2adedgspthlem2  28188  frgregordn0  28317  lsatn0  29636  lsatspn0  29637  lkrlspeqN  29808  cvlsupr2  29980  dalem25  30334  4atexlemcnd  30708  ltrncnvnid  30763  trlator0  30807  ltrnnidn  30810  trlnid  30815  cdleme3b  30865  cdleme11l  30905  cdleme16b  30915  cdleme35h2  31093  cdleme38n  31100  cdlemg8c  31265  cdlemg11a  31273  cdlemg12e  31283  cdlemg18a  31314  trlcoat  31359  trlcone  31364  tendo1ne0  31464  cdleml9  31620  dvheveccl  31749  dihmeetlem13N  31956  dihlspsnat  31970  dihpN  31973  dihatexv  31975  dochsat  32020  dochkrshp  32023  dochkr1  32115  lcfrlem28  32207  lcfrlem32  32211  mapdn0  32306  mapdpglem11  32319  mapdpglem16  32324
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 178  df-ne 2600
  Copyright terms: Public domain W3C validator