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

Theorem necon3bid 2602
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 2569 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2601 . 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 1649    =/= wne 2567
This theorem is referenced by:  nebi  2638  frxp  6415  iinon  6561  fodomfib  7345  wemapso  7476  wemapso2  7477  infpssrlem4  8142  ttukeylem6  8350  fodomb  8360  tskcard  8612  addneintrd  9229  addneintr2d  9230  negne0bd  9360  negned  9364  subne0d  9376  subne0ad  9378  subneintrd  9411  subneintr2d  9413  divne0b  9645  div2neg  9693  divne1d  9757  div2sub  9795  xaddass2  10785  xadddi2  10832  seqf1olem1  11317  expne0  11366  sqne0  11403  hashnncl  11600  hashgt0  11617  cjne0  11923  recval  12081  absgt0  12083  abs1m  12094  abslem2  12098  sqreulem  12118  sqreu  12119  absne0d  12204  geoserg  12600  geolim  12602  geolim2  12603  georeclim  12604  geoisum1c  12612  tanval2  12689  tanaddlem  12722  tanadd  12723  4sqlem11  13278  ipodrsima  14546  sylow1lem4  15190  dprdf1o  15545  dprd2da  15555  abvne0  15870  rrgsupp  16306  gzrngunit  16719  chrnzr  16766  obsne0  16907  cnhaus  17372  hauscmplem  17423  fsubbas  17852  metn0  18343  nmne0  18618  iccpnfhmeo  18923  ipcau2  19144  dvcnvlem  19813  dvlip  19830  ftc1lem5  19877  mdegldg  19942  ply1divmo  20011  ig1peu  20047  ig1pdvds  20052  dgrmul  20141  coecj  20149  plydivlem4  20166  vieta1lem2  20181  vieta1  20182  aareccl  20196  geolim3  20209  abelthlem2  20301  abelthlem7  20307  tanregt0  20394  logne0  20450  tanarg  20467  logtayl  20504  abscxp2  20537  cxpsqr  20547  abscxpbnd  20590  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  lawcos  20611  logrec  20614  isosctr  20618  asinlem  20661  atandm2  20670  atandm4  20672  2efiatan  20711  tanatan  20712  atandmtan  20713  dvatan  20728  mersenne  20964  perfectlem2  20967  dchrinv  20998  dchrptlem2  21002  dchrsum2  21005  sumdchr2  21007  lgsabs1  21071  dchrisum0re  21160  rngoridfz  21976  nvgt0  22117  nv1  22118  nmlnogt0  22251  nmblolbii  22253  blocnilem  22258  normne0  22585  normcan  23031  nmlnopne0  23455  nmophmi  23487  riesz3i  23518  esumpcvgval  24421  ballotlemfrcn0  24740  erdszelem9  24838  sltval2  25524  colinearalg  25753  axsegconlem6  25765  axsegconlem9  25768  ax5seglem5  25776  axlowdimlem14  25798  segcon2  25943  outsideofeu  25969  smprngopr  26552  isfldidl2  26569  isdmn3  26574  jm2.19  26954  jm2.26lem3  26962  kelac1  27029  mpaaeu  27223  f1omvdmvd  27254  f1omvdcnv  27255  f1omvdconj  27257  pmtrfmvdn0  27271  pr1nebg  27945  onetansqsecsq  28218  bnj168  28803  lsat0cv  29516  lcvexchlem1  29517  lsatcvat2  29534  lkrshp  29588  lkrshp3  29589  lkrpssN  29646  cvrat2  29911  atcvrneN  29912  atcvrj2b  29914  2llnmat  30006  2lnat  30266  pmapjat1  30335  pclfinclN  30432  lautlt  30573  ltrn11at  30629  ltrnatneq  30664  trlcone  31210  tendoconid  31311  tendotr  31312  cdleml3N  31460  dochsordN  31857  dochn0nv  31858  djhcvat42  31898  dochsatshp  31934  lcfl8b  31987  lclkrlem2a  31990  lcfrlem9  32033  mapdsord  32138  mapdncol  32153  mapdpglem29  32183  mapdindp1  32203  hdmapnzcl  32331  hdmaprnlem1N  32335  hdmaprnlem3N  32336  hdmaprnlem3uN  32337  hdmaprnlem9N  32343  hdmap14lem9  32362  hgmapval1  32379  hgmapadd  32380  hgmapmul  32381  hgmaprnlem1N  32382  hdmaplkr  32399  hdmapip1  32402  hgmapvvlem1  32409  hgmapvvlem2  32410  hgmapvvlem3  32411
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 2569
  Copyright terms: Public domain W3C validator