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

Theorem necon3bid 2494
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 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3bid.1 . . 3  |-  ( ph  ->  ( A  =  B  <-> 
C  =  D ) )
32necon3bbid 2493 . 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 1632    =/= wne 2459
This theorem is referenced by:  nebi  2530  frxp  6241  iinon  6373  fodomfib  7152  wemapso  7282  wemapso2  7283  infpssrlem4  7948  ttukeylem6  8157  fodomb  8167  tskcard  8419  addneintrd  9035  addneintr2d  9036  negne0bd  9166  negned  9170  subne0d  9182  subne0ad  9184  subneintrd  9217  subneintr2d  9219  divne0b  9451  div2neg  9499  divne1d  9563  div2sub  9601  xaddass2  10586  xadddi2  10633  seqf1olem1  11101  expne0  11149  sqne0  11186  hashnncl  11370  cjne0  11664  recval  11822  absgt0  11824  abs1m  11835  abslem2  11839  sqreulem  11859  sqreu  11860  absne0d  11945  rlimuni  12040  climuni  12042  geoserg  12340  geolim  12342  geolim2  12343  georeclim  12344  geoisum1c  12352  tanval2  12429  tanaddlem  12462  tanadd  12463  4sqlem11  13018  ipodrsima  14284  sylow1lem4  14928  dprdf1o  15283  dprd2da  15293  abvne0  15608  rrgsupp  16048  gzrngunit  16453  chrnzr  16500  obsne0  16641  cnhaus  17098  hauscmplem  17149  fsubbas  17578  metn0  17940  nmne0  18156  reperflem  18339  iccpnfhmeo  18459  evth  18473  ipcau2  18680  dvlem  19262  dvconst  19282  dvid  19283  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvcjbr  19314  dvrec  19320  dvcnvlem  19339  dvferm2lem  19349  dvlip  19356  ftc1lem5  19403  mdegldg  19468  ply1divmo  19537  ig1peu  19573  ig1pdvds  19578  dgrmul  19667  coecj  19675  plydivlem4  19692  vieta1lem2  19707  vieta1  19708  aareccl  19722  geolim3  19735  taylthlem2  19769  ulmdvlem1  19793  abelthlem2  19824  abelthlem7  19830  tanregt0  19917  logne0  19972  tanarg  19986  logtayl  20023  abscxp2  20056  cxpsqr  20066  abscxpbnd  20109  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  ang180lem5  20127  ang180  20128  lawcos  20130  logrec  20133  isosctrlem3  20136  isosctr  20137  asinlem  20180  atandm2  20189  atandm4  20191  2efiatan  20230  tanatan  20231  atandmtan  20232  dvatan  20247  mersenne  20482  perfectlem2  20485  dchrinv  20516  dchrptlem2  20520  dchrsum2  20523  sumdchr2  20525  lgsabs1  20589  dchrisum0re  20678  nvgt0  21257  nv1  21258  nmlnogt0  21391  nmblolbii  21393  blocnilem  21398  normne0  21725  normcan  22171  nmlnopne0  22595  nmophmi  22627  riesz3i  22658  ballotlemfrcn0  23104  hashgt0  23402  esumpcvgval  23461  erdszelem9  23745  sltval2  24381  brbtwn2  24605  colinearalg  24610  axsegconlem6  24622  axsegconlem9  24625  ax5seglem5  24633  axlowdimlem14  24655  axcontlem8  24671  segcon2  24800  outsideofeu  24826  rngoridfz  25540  clscnc  26113  smprngopr  26780  isfldidl2  26797  isdmn3  26802  pellexlem6  27022  jm2.19  27189  jm2.26lem3  27197  kelac1  27264  mpaaeu  27458  f1omvdmvd  27489  f1omvdcnv  27490  f1omvdconj  27492  pmtrfmvdn0  27506  onetansqsecsq  28485  bnj168  29074  lsat0cv  29845  lcvexchlem1  29846  lsatcvat2  29863  lkrshp  29917  lkrshp3  29918  lkrpssN  29975  cvrat2  30240  atcvrneN  30241  atcvrj2b  30243  2llnmat  30335  2lnat  30595  pmapjat1  30664  pclfinclN  30761  lautlt  30902  ltrn11at  30958  ltrnatneq  30993  trlcone  31539  tendoconid  31640  tendotr  31641  cdleml3N  31789  dochsordN  32186  dochn0nv  32187  djhcvat42  32227  dochsatshp  32263  lcfl8b  32316  lclkrlem2a  32319  lcfrlem9  32362  mapdsord  32467  mapdncol  32482  mapdpglem29  32512  mapdindp1  32532  hdmapnzcl  32660  hdmaprnlem1N  32664  hdmaprnlem3N  32665  hdmaprnlem3uN  32666  hdmaprnlem9N  32672  hdmap14lem9  32691  hgmapval1  32708  hgmapadd  32709  hgmapmul  32710  hgmaprnlem1N  32711  hdmaplkr  32728  hdmapip1  32731  hgmapvvlem1  32738  hgmapvvlem2  32739  hgmapvvlem3  32740
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