Theorem necon3bid 3013

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	⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))

Assertion

Ref	Expression
necon3bid	⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Proof of Theorem necon3bid

Step	Hyp	Ref	Expression
1		df-ne 2970	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 3006	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	syl5bb 275	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   = wceq 1601   ≠ wne 2969

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 199  df-ne 2970

This theorem is referenced by:  neeq1d  3028  neeq2d  3029  neeq12d  3030  nebi  3049  pr1nebg  4619  f1dom3fv3dif  6797  frxp  7568  suppval1  7582  iinon  7720  fodomfib  8528  wemapso  8745  wemapso2lem  8746  infpssrlem4  9463  ttukeylem6  9671  fodomb  9683  tskcard  9938  addneintrd  10583  addneintr2d  10584  negne0bd  10727  negned  10731  subne0d  10743  subne0ad  10745  subneintrd  10778  subneintr2d  10780  divne0b  11044  div2neg  11098  divne1d  11162  div2sub  11200  xaddass2  12392  xadddi2  12439  seqf1olem1  13158  expne0  13209  sqne0  13248  hashneq0  13470  hashnncl  13472  hashgt0  13492  swrdn0OLD  13747  pfxn0  13795  cjne0  14310  recval  14469  absgt0  14471  abs1m  14482  abslem2  14486  sqreulem  14506  sqreu  14507  absne0d  14594  geoserg  15002  geolim  15005  geolim2  15006  georeclim  15007  geoisum1c  15015  tanval2  15265  tanaddlem  15298  tanadd  15299  4sqlem11  16063  ipodrsima  17551  f1omvdmvd  18246  f1omvdcnv  18247  f1omvdconj  18249  pmtrfmvdn0  18265  sylow1lem4  18400  dprdf1o  18818  dprd2da  18828  ringinvnz1ne0  18979  abvne0  19219  rrgsupp  19688  gzrngunit  20208  chrnzr  20274  obsne0  20468  mdetdiaglem  20809  cnhaus  21566  hauscmplem  21618  fsubbas  22079  metn0  22573  nmne0  22831  nmgt0  22842  iccpnfhmeo  23152  ncvs1  23364  ipcau2  23440  dvcnvlem  24176  dvlip  24193  ftc1lem5  24240  mdegldg  24263  ply1divmo  24332  ig1peu  24368  ig1pdvds  24373  dgrmul  24463  coecj  24471  plydivlem4  24488  vieta1lem2  24503  vieta1  24504  aareccl  24518  geolim3  24531  abelthlem2  24623  abelthlem7  24629  tanregt0  24723  tanarg  24802  logtayl  24843  abscxp2  24876  cxpsqrt  24886  abscxpbnd  24934  logrec  24941  ang180lem1  24987  ang180lem2  24988  ang180lem3  24989  lawcos  24994  isosctr  24999  asinlem  25046  atandm2  25055  atandm4  25057  2efiatan  25096  tanatan  25097  atandmtan  25098  dvatan  25113  mersenne  25404  perfectlem2  25407  dchrinv  25438  dchrptlem2  25442  dchrsum2  25445  sumdchr2  25447  lgsabs1  25513  dchrisum0re  25654  tgcgrneq  25834  footex  26069  colinearalg  26259  axsegconlem6  26271  axsegconlem9  26274  ax5seglem5  26282  axlowdimlem14  26304  wlkn0  26968  cyclnspth  27152  iswwlksnx  27189  wwlksm1edg  27230  wwlksm1edgOLD  27231  wspthsnonn0vne  27297  umgrclwwlkge2  27371  clwwisshclwws  27404  hashecclwwlkn1  27475  umgrhashecclwwlk  27476  frgrregord013  27827  frgrogt3nreg  27829  friendshipgt3  27830  nvgt0  28101  nv1  28102  nmlnogt0  28224  nmblolbii  28226  blocnilem  28231  normne0  28559  normcan  29007  nmlnopne0  29430  nmophmi  29462  riesz3i  29493  ogrpsublt  30284  esumpcvgval  30738  ballotlemfrcn0  31190  signsply0  31228  signstfvn  31246  signsvtn0  31247  signsvtn0OLD  31248  signstfvneq0  31250  signstfveq0a  31254  signshnz  31270  bnj168  31398  erdszelem9  31780  sltval2  32398  segcon2  32801  outsideofeu  32827  heicant  34070  smprngopr  34475  isfldidl2  34492  isdmn3  34497  lsat0cv  35187  lcvexchlem1  35188  lsatcvat2  35205  lkrshp  35259  lkrshp3  35260  lkrpssN  35317  cvrat2  35583  atcvrneN  35584  atcvrj2b  35586  2llnmat  35678  2lnat  35938  pmapjat1  36007  pclfinclN  36104  lautlt  36245  ltrn11at  36301  ltrnatneq  36336  trlcone  36882  tendoconid  36983  tendotr  36984  cdleml3N  37132  dochsordN  37528  dochn0nv  37529  djhcvat42  37569  dochsatshp  37605  lcfl8b  37658  lclkrlem2a  37661  lcfrlem9  37704  mapdsord  37809  mapdncol  37824  mapdpglem29  37854  mapdindp1  37874  hdmapnzcl  37999  hdmaprnlem1N  38003  hdmaprnlem3N  38004  hdmaprnlem3uN  38005  hdmaprnlem9N  38011  hdmap14lem9  38030  hgmapval1  38047  hgmapadd  38048  hgmapmul  38049  hgmaprnlem1N  38050  hdmaplkr  38067  hdmapip1  38070  hgmapvvlem1  38077  hgmapvvlem2  38078  hgmapvvlem3  38079  jm2.19  38519  jm2.26lem3  38527  kelac1  38592  mpaaeu  38679  radcnvrat  39469  binomcxplemnotnn0  39511  sqrtnegnre  42349  paireqne  42450  fmtnoprmfac1lem  42497  requad01  42559  requad2  42561  perfectALTVlem2  42656  nnsgrpnmnd  42833  rrx2pnedifcoorneor  43452  rrx2pnedifcoorneorr  43453  eenglngeehlnmlem2  43474  onetansqsecsq  43610