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

Theorem necon3bid 2481
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 2448 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2480 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  C  =/=  D
) )
41, 3syl5bb 248 1  |-  ( ph  ->  ( A  =/=  B  <->  C  =/=  D ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  nebi  2517  frxp  6225  iinon  6357  fodomfib  7136  wemapso  7266  wemapso2  7267  infpssrlem4  7932  ttukeylem6  8141  fodomb  8151  tskcard  8403  addneintrd  9019  addneintr2d  9020  negne0bd  9150  negned  9154  subne0d  9166  subne0ad  9168  subneintrd  9201  subneintr2d  9203  divne0b  9435  div2neg  9483  divne1d  9547  div2sub  9585  xaddass2  10570  xadddi2  10617  seqf1olem1  11085  expne0  11133  sqne0  11170  hashnncl  11354  cjne0  11648  recval  11806  absgt0  11808  abs1m  11819  abslem2  11823  sqreulem  11843  sqreu  11844  absne0d  11929  rlimuni  12024  climuni  12026  geoserg  12324  geolim  12326  geolim2  12327  georeclim  12328  geoisum1c  12336  tanval2  12413  tanaddlem  12446  tanadd  12447  4sqlem11  13002  ipodrsima  14268  sylow1lem4  14912  dprdf1o  15267  dprd2da  15277  abvne0  15592  rrgsupp  16032  gzrngunit  16437  chrnzr  16484  obsne0  16625  cnhaus  17082  hauscmplem  17133  fsubbas  17562  metn0  17924  nmne0  18140  reperflem  18323  iccpnfhmeo  18443  evth  18457  ipcau2  18664  dvlem  19246  dvconst  19266  dvid  19267  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvcjbr  19298  dvrec  19304  dvcnvlem  19323  dvferm2lem  19333  dvlip  19340  ftc1lem5  19387  mdegldg  19452  ply1divmo  19521  ig1peu  19557  ig1pdvds  19562  dgrmul  19651  coecj  19659  plydivlem4  19676  vieta1lem2  19691  vieta1  19692  aareccl  19706  geolim3  19719  taylthlem2  19753  ulmdvlem1  19777  abelthlem2  19808  abelthlem7  19814  tanregt0  19901  logne0  19956  tanarg  19970  logtayl  20007  abscxp2  20040  cxpsqr  20050  abscxpbnd  20093  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  ang180lem5  20111  ang180  20112  lawcos  20114  logrec  20117  isosctrlem3  20120  isosctr  20121  asinlem  20164  atandm2  20173  atandm4  20175  2efiatan  20214  tanatan  20215  atandmtan  20216  dvatan  20231  mersenne  20466  perfectlem2  20469  dchrinv  20500  dchrptlem2  20504  dchrsum2  20507  sumdchr2  20509  lgsabs1  20573  dchrisum0re  20662  nvgt0  21241  nv1  21242  nmlnogt0  21375  nmblolbii  21377  blocnilem  21382  normne0  21709  normcan  22155  nmlnopne0  22579  nmophmi  22611  riesz3i  22642  ballotlemfrcn0  23088  hashgt0  23387  esumpcvgval  23446  erdszelem9  23730  sltval2  24310  brbtwn2  24533  colinearalg  24538  axsegconlem6  24550  axsegconlem9  24553  ax5seglem5  24561  axlowdimlem14  24583  axcontlem8  24599  segcon2  24728  outsideofeu  24754  rngoridfz  25437  clscnc  26010  smprngopr  26677  isfldidl2  26694  isdmn3  26699  pellexlem6  26919  jm2.19  27086  jm2.26lem3  27094  kelac1  27161  mpaaeu  27355  f1omvdmvd  27386  f1omvdcnv  27387  f1omvdconj  27389  pmtrfmvdn0  27403  onetansqsecsq  28231  bnj168  28758  lsat0cv  29223  lcvexchlem1  29224  lsatcvat2  29241  lkrshp  29295  lkrshp3  29296  lkrpssN  29353  cvrat2  29618  atcvrneN  29619  atcvrj2b  29621  2llnmat  29713  2lnat  29973  pmapjat1  30042  pclfinclN  30139  lautlt  30280  ltrn11at  30336  ltrnatneq  30371  trlcone  30917  tendoconid  31018  tendotr  31019  cdleml3N  31167  dochsordN  31564  dochn0nv  31565  djhcvat42  31605  dochsatshp  31641  lcfl8b  31694  lclkrlem2a  31697  lcfrlem9  31740  mapdsord  31845  mapdncol  31860  mapdpglem29  31890  mapdindp1  31910  hdmapnzcl  32038  hdmaprnlem1N  32042  hdmaprnlem3N  32043  hdmaprnlem3uN  32044  hdmaprnlem9N  32050  hdmap14lem9  32069  hgmapval1  32086  hgmapadd  32087  hgmapmul  32088  hgmaprnlem1N  32089  hdmaplkr  32106  hdmapip1  32109  hgmapvvlem1  32116  hgmapvvlem2  32117  hgmapvvlem3  32118
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 2448
  Copyright terms: Public domain W3C validator