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

Theorem necon3bid 2636
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3bid.1  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
Assertion
Ref Expression
necon3bid  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )

Proof of Theorem necon3bid
StepHypRef Expression
1 df-ne 2601 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2635 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  C  =/=  D
) )
41, 3syl5bb 249 1  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1652    =/= wne 2599
This theorem is referenced by:  nebi  2675  frxp  6456  iinon  6602  fodomfib  7386  wemapso  7520  wemapso2  7521  infpssrlem4  8186  ttukeylem6  8394  fodomb  8404  tskcard  8656  addneintrd  9273  addneintr2d  9274  negne0bd  9404  negned  9408  subne0d  9420  subne0ad  9422  subneintrd  9455  subneintr2d  9457  divne0b  9689  div2neg  9737  divne1d  9801  div2sub  9839  xaddass2  10829  xadddi2  10876  seqf1olem1  11362  expne0  11411  sqne0  11448  hashnncl  11645  hashgt0  11662  cjne0  11968  recval  12126  absgt0  12128  abs1m  12139  abslem2  12143  sqreulem  12163  sqreu  12164  absne0d  12249  geoserg  12645  geolim  12647  geolim2  12648  georeclim  12649  geoisum1c  12657  tanval2  12734  tanaddlem  12767  tanadd  12768  4sqlem11  13323  ipodrsima  14591  sylow1lem4  15235  dprdf1o  15590  dprd2da  15600  abvne0  15915  rrgsupp  16351  gzrngunit  16764  chrnzr  16811  obsne0  16952  cnhaus  17418  hauscmplem  17469  fsubbas  17899  metn0  18390  nmne0  18665  iccpnfhmeo  18970  ipcau2  19191  dvcnvlem  19860  dvlip  19877  ftc1lem5  19924  mdegldg  19989  ply1divmo  20058  ig1peu  20094  ig1pdvds  20099  dgrmul  20188  coecj  20196  plydivlem4  20213  vieta1lem2  20228  vieta1  20229  aareccl  20243  geolim3  20256  abelthlem2  20348  abelthlem7  20354  tanregt0  20441  logne0  20497  tanarg  20514  logtayl  20551  abscxp2  20584  cxpsqr  20594  abscxpbnd  20637  ang180lem1  20651  ang180lem2  20652  ang180lem3  20653  lawcos  20658  logrec  20661  isosctr  20665  asinlem  20708  atandm2  20717  atandm4  20719  2efiatan  20758  tanatan  20759  atandmtan  20760  dvatan  20775  mersenne  21011  perfectlem2  21014  dchrinv  21045  dchrptlem2  21049  dchrsum2  21052  sumdchr2  21054  lgsabs1  21118  dchrisum0re  21207  rngoridfz  22023  nvgt0  22164  nv1  22165  nmlnogt0  22298  nmblolbii  22300  blocnilem  22305  normne0  22632  normcan  23078  nmlnopne0  23502  nmophmi  23534  riesz3i  23565  esumpcvgval  24468  ballotlemfrcn0  24787  erdszelem9  24885  sltval2  25611  colinearalg  25849  axsegconlem6  25861  axsegconlem9  25864  ax5seglem5  25872  axlowdimlem14  25894  segcon2  26039  outsideofeu  26065  smprngopr  26662  isfldidl2  26679  isdmn3  26684  jm2.19  27064  jm2.26lem3  27072  kelac1  27138  mpaaeu  27332  f1omvdmvd  27363  f1omvdcnv  27364  f1omvdconj  27366  pmtrfmvdn0  27380  pr1nebg  28057  wrdlenge2n0  28176  swrdtrcfv0  28195  swrdtrcfvl  28265  onetansqsecsq  28504  bnj168  29097  lsat0cv  29831  lcvexchlem1  29832  lsatcvat2  29849  lkrshp  29903  lkrshp3  29904  lkrpssN  29961  cvrat2  30226  atcvrneN  30227  atcvrj2b  30229  2llnmat  30321  2lnat  30581  pmapjat1  30650  pclfinclN  30747  lautlt  30888  ltrn11at  30944  ltrnatneq  30979  trlcone  31525  tendoconid  31626  tendotr  31627  cdleml3N  31775  dochsordN  32172  dochn0nv  32173  djhcvat42  32213  dochsatshp  32249  lcfl8b  32302  lclkrlem2a  32305  lcfrlem9  32348  mapdsord  32453  mapdncol  32468  mapdpglem29  32498  mapdindp1  32518  hdmapnzcl  32646  hdmaprnlem1N  32650  hdmaprnlem3N  32651  hdmaprnlem3uN  32652  hdmaprnlem9N  32658  hdmap14lem9  32677  hgmapval1  32694  hgmapadd  32695  hgmapmul  32696  hgmaprnlem1N  32697  hdmaplkr  32714  hdmapip1  32717  hgmapvvlem1  32724  hgmapvvlem2  32725  hgmapvvlem3  32726
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 2601
  Copyright terms: Public domain W3C validator