Theorem necon3bid 2838

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

Step	Hyp	Ref	Expression
1		df-ne 2795	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2831	. 2 |- ( ph -> ( -. A = B <-> C =/= D ) )
4	1, 3	syl5bb 272	1 |- ( ph -> ( A =/= B <-> C =/= D ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  neeq1d  2853  neeq2d  2854  neeq12d  2855  nebi  2874  pr1nebg  4391  f1dom3fv3dif  6525  frxp  7287  suppval1  7301  iinon  7437  fodomfib  8240  wemapso  8456  wemapso2lem  8457  infpssrlem4  9128  ttukeylem6  9336  fodomb  9348  tskcard  9603  addneintrd  10243  addneintr2d  10244  negne0bd  10385  negned  10389  subne0d  10401  subne0ad  10403  subneintrd  10436  subneintr2d  10438  divne0b  10696  div2neg  10748  divne1d  10812  div2sub  10850  xaddass2  12080  xadddi2  12127  seqf1olem1  12840  expne0  12891  sqne0  12930  hashneq0  13155  hashnncl  13157  hashgt0  13177  swrdn0  13430  cjne0  13903  recval  14062  absgt0  14064  abs1m  14075  abslem2  14079  sqreulem  14099  sqreu  14100  absne0d  14186  geoserg  14598  geolim  14601  geolim2  14602  georeclim  14603  geoisum1c  14611  tanval2  14863  tanaddlem  14896  tanadd  14897  4sqlem11  15659  ipodrsima  17165  f1omvdmvd  17863  f1omvdcnv  17864  f1omvdconj  17866  pmtrfmvdn0  17882  sylow1lem4  18016  dprdf1o  18431  dprd2da  18441  ringinvnz1ne0  18592  abvne0  18827  rrgsupp  19291  gzrngunit  19812  chrnzr  19878  obsne0  20069  mdetdiaglem  20404  cnhaus  21158  hauscmplem  21209  fsubbas  21671  metn0  22165  nmne0  22423  nmgt0  22434  iccpnfhmeo  22744  ncvs1  22957  ipcau2  23033  dvcnvlem  23739  dvlip  23756  ftc1lem5  23803  mdegldg  23826  ply1divmo  23895  ig1peu  23931  ig1pdvds  23936  dgrmul  24026  coecj  24034  plydivlem4  24051  vieta1lem2  24066  vieta1  24067  aareccl  24081  geolim3  24094  abelthlem2  24186  abelthlem7  24192  tanregt0  24285  tanarg  24365  logtayl  24406  abscxp2  24439  cxpsqrt  24449  abscxpbnd  24494  logrec  24501  ang180lem1  24539  ang180lem2  24540  ang180lem3  24541  lawcos  24546  isosctr  24551  asinlem  24595  atandm2  24604  atandm4  24606  2efiatan  24645  tanatan  24646  atandmtan  24647  dvatan  24662  mersenne  24952  perfectlem2  24955  dchrinv  24986  dchrptlem2  24990  dchrsum2  24993  sumdchr2  24995  lgsabs1  25061  dchrisum0re  25202  tgcgrneq  25378  footex  25613  colinearalg  25790  axsegconlem6  25802  axsegconlem9  25805  ax5seglem5  25813  axlowdimlem14  25835  wlkn0  26516  cyclnspth  26695  iswwlksnx  26731  wwlksm1edg  26767  wspthsnonn0vne  26813  isclwwlksnx  26889  umgrclwwlksge2  26912  clwwisshclwws  26928  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  frgrregord013  27253  frgrogt3nreg  27255  friendshipgt3  27256  nvgt0  27529  nv1  27530  nmlnogt0  27652  nmblolbii  27654  blocnilem  27659  normne0  27987  normcan  28435  nmlnopne0  28858  nmophmi  28890  riesz3i  28921  ogrpsublt  29722  esumpcvgval  30140  ballotlemfrcn0  30591  signsply0  30628  signstfvn  30646  signsvtn0  30647  signstfvneq0  30649  signstfveq0a  30653  signshnz  30668  bnj168  30798  erdszelem9  31181  sltval2  31809  segcon2  32212  outsideofeu  32238  heicant  33444  smprngopr  33851  isfldidl2  33868  isdmn3  33873  lsat0cv  34320  lcvexchlem1  34321  lsatcvat2  34338  lkrshp  34392  lkrshp3  34393  lkrpssN  34450  cvrat2  34715  atcvrneN  34716  atcvrj2b  34718  2llnmat  34810  2lnat  35070  pmapjat1  35139  pclfinclN  35236  lautlt  35377  ltrn11at  35433  ltrnatneq  35469  trlcone  36016  tendoconid  36117  tendotr  36118  cdleml3N  36266  dochsordN  36663  dochn0nv  36664  djhcvat42  36704  dochsatshp  36740  lcfl8b  36793  lclkrlem2a  36796  lcfrlem9  36839  mapdsord  36944  mapdncol  36959  mapdpglem29  36989  mapdindp1  37009  hdmapnzcl  37137  hdmaprnlem1N  37141  hdmaprnlem3N  37142  hdmaprnlem3uN  37143  hdmaprnlem9N  37149  hdmap14lem9  37168  hgmapval1  37185  hgmapadd  37186  hgmapmul  37187  hgmaprnlem1N  37188  hdmaplkr  37205  hdmapip1  37208  hgmapvvlem1  37215  hgmapvvlem2  37216  hgmapvvlem3  37217  jm2.19  37560  jm2.26lem3  37568  kelac1  37633  mpaaeu  37720  radcnvrat  38513  binomcxplemnotnn0  38555  fmtnoprmfac1lem  41476  perfectALTVlem2  41631  nnsgrpnmnd  41818  onetansqsecsq  42502