Theorem necon3bid 3002

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 2959	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 2995	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	bitrid 286	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  neeq1d  3017  neeq2d  3018  neeq12d  3019  nebi  3038  pr1nebg  4823  f1dom3fv3dif  7266  frxp  8118  frxp2  8136  frxp3  8143  suppval1  8158  iinon  8323  fodomfib  9284  wemapso  9509  wemapso2lem  9510  infpssrlem4  10285  ttukeylem6  10493  fodomb  10505  tskcard  10761  addneintrd  11412  addneintr2d  11413  negne0bd  11557  negned  11561  subne0d  11573  subne0ad  11575  subneintrd  11608  subneintr2d  11610  divne0b  11878  div2neg  11933  divne1d  11997  div2sub  12035  xaddass2  13271  xadddi2  13318  seqf1olem1  14073  expne0  14125  sqne0  14155  hashneq0  14396  hashnncl  14398  hashgt0  14420  ccat1st1st  14662  pfxn0  14720  cjne0  15210  recval  15370  absgt0  15372  abs1m  15383  abslem2  15387  sqreulem  15407  sqreu  15408  absne0d  15497  geoserg  15916  geolim  15920  geolim2  15921  georeclim  15922  geoisum1c  15930  tanval2  16184  tanaddlem  16217  tanadd  16218  4sqlem11  17010  ipodrsima  18592  chnind  18672  chnub  18673  f1omvdmvd  19508  f1omvdcnv  19509  f1omvdconj  19511  pmtrfmvdn0  19527  sylow1lem4  19666  dprdf1o  20099  dprd2da  20109  ogrpsublt  20207  ringinvnz1ne0  20379  rrgsupp  20800  abvne0  20922  isfieldidl2  21387  gzrngunit  21583  chrnzr  21680  obsne0  21875  mdetdiaglem  22755  cnhaus  23511  hauscmplem  23563  fsubbas  24024  metn0  24517  nmne0  24776  nmgt0  24787  iccpnfhmeo  25104  ncvs1  25316  ipcau2  25393  dvcnvlem  26135  dvlip  26152  ftc1lem5  26199  mdegldg  26223  ply1divmo  26293  ig1peu  26332  ig1pdvds  26337  dgrmul  26427  coecj  26435  coecjOLD  26437  plydivlem4  26457  vieta1lem2  26472  vieta1  26473  aareccl  26489  geolim3  26502  abelthlem2  26595  abelthlem7  26601  tanregt0  26704  tanarg  26784  logtayl  26825  abscxp2  26858  cxpsqrt  26868  abscxpbnd  26918  logrec  26928  ang180lem1  26974  ang180lem2  26975  ang180lem3  26976  lawcos  26981  isosctr  26986  asinlem  27033  atandm2  27042  atandm4  27044  2efiatan  27083  tanatan  27084  atandmtan  27085  dvatan  27100  mersenne  27391  perfectlem2  27394  dchrinv  27425  dchrptlem2  27429  dchrsum2  27432  sumdchr2  27434  lgsabs1  27500  dchrisum0re  27677  ltsval2  27820  bday1  28007  cuteq1  28010  n0subs2  28557  tgcgrneq  28752  mirlni  28972  footexALT  28998  footexlem1  28999  footexlem2  29000  prlngsymquadlem  29213  colinearalg  29260  axsegconlem6  29272  axsegconlem9  29275  ax5seglem5  29283  axlowdimlem14  29305  wlkn0  29970  cyclnspth  30150  iswwlksnx  30189  wwlksm1edg  30230  wspthsnonn0vne  30266  umgrclwwlkge2  30342  clwwisshclwws  30366  hashecclwwlkn1  30428  umgrhashecclwwlk  30429  frgrregord013  30746  frgrogt3nreg  30748  friendshipgt3  30749  nrt2irr  30824  nvgt0  31026  nv1  31027  nmlnogt0  31149  nmblolbii  31151  blocnilem  31156  normne0  31482  normcan  31928  nmlnopne0  32351  nmophmi  32383  riesz3i  32414  hashne0  33154  wrdpmtrlast  33413  cycpmco2lem6  33451  1arithidom  33827  ply1unit  33865  m1pmeq  33875  minplyirredlem  34100  constrrtcclem  34124  constrconj  34135  iconstr  34156  zarclssn  34263  esumpcvgval  34468  ballotlemfrcn0  34920  signsply0  34938  signstfvn  34956  signsvtn0  34957  signstfvneq0  34959  signstfveq0a  34963  signshnz  34978  bnj168  35119  nummin  35484  usgrgt2cycl  35622  erdszelem9  35691  segcon2  36597  outsideofeu  36623  heicant  38326  smprngopr  38723  isfldidl2  38740  isdmn3  38745  lsat0cv  39827  lcvexchlem1  39828  lsatcvat2  39845  lkrshp  39899  lkrshp3  39900  lkrpssN  39957  cvrat2  40223  atcvrneN  40224  atcvrj2b  40226  2llnmat  40318  2lnat  40578  pmapjat1  40647  pclfinclN  40744  lautlt  40885  ltrn11at  40941  ltrnatneq  40976  trlcone  41522  tendoconid  41623  tendotr  41624  cdleml3N  41772  dochsordN  42168  dochn0nv  42169  djhcvat42  42209  dochsatshp  42245  lcfl8b  42298  lclkrlem2a  42301  lcfrlem9  42344  mapdsord  42449  mapdncol  42464  mapdpglem29  42494  mapdindp1  42514  hdmapnzcl  42639  hdmaprnlem1N  42643  hdmaprnlem3N  42644  hdmaprnlem3uN  42645  hdmaprnlem9N  42651  hdmap14lem9  42670  hgmapval1  42687  hgmapadd  42688  hgmapmul  42689  hgmaprnlem1N  42690  hdmaplkr  42707  hdmapip1  42710  hgmapvvlem1  42717  hgmapvvlem2  42718  hgmapvvlem3  42719  fldhmf1  42877  aks6d1c2p2  42906  aks6d1c5lem2  42925  aks6d1c6lem3  42959  redivne0bd  43231  fsuppind  43342  jm2.19  43740  jm2.26lem3  43748  kelac1  43810  mpaaeu  43897  radcnvrat  45044  binomcxplemnotnn0  45086  sqrtnegnre  48064  paireqne  48280  fmtnoprmfac1lem  48336  requad01  48406  requad2  48408  perfectALTVlem2  48507  nnsgrpnmnd  48963  isidom3  49130  rrx2pnedifcoorneor  49516  rrx2pnedifcoorneorr  49517  eenglngeehlnmlem2  49538  fdomne0  49648  oppcendc  49816  onetansqsecsq  50559