Theorem necon3bid 3060

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 3017	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 3053	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	syl5bb 285	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1533   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  neeq1d  3075  neeq2d  3076  neeq12d  3077  nebi  3096  pr1nebg  4787  f1dom3fv3dif  7025  frxp  7819  suppval1  7835  iinon  7976  fodomfib  8797  wemapso  9014  wemapso2lem  9015  infpssrlem4  9727  ttukeylem6  9935  fodomb  9947  tskcard  10202  addneintrd  10846  addneintr2d  10847  negne0bd  10989  negned  10993  subne0d  11005  subne0ad  11007  subneintrd  11040  subneintr2d  11042  divne0b  11308  div2neg  11362  divne1d  11426  div2sub  11464  xaddass2  12642  xadddi2  12689  seqf1olem1  13408  expne0  13459  sqne0  13488  hashneq0  13724  hashnncl  13726  hashgt0  13748  ccat1st1st  13983  pfxn0  14047  cjne0  14521  recval  14681  absgt0  14683  abs1m  14694  abslem2  14698  sqreulem  14718  sqreu  14719  absne0d  14806  geoserg  15220  geolim  15225  geolim2  15226  georeclim  15227  geoisum1c  15235  tanval2  15485  tanaddlem  15518  tanadd  15519  4sqlem11  16290  ipodrsima  17774  f1omvdmvd  18570  f1omvdcnv  18571  f1omvdconj  18573  pmtrfmvdn0  18589  sylow1lem4  18725  dprdf1o  19153  dprd2da  19163  ringinvnz1ne0  19341  abvne0  19597  rrgsupp  20063  mhpinvcl  20338  gzrngunit  20610  chrnzr  20676  obsne0  20868  mdetdiaglem  21206  cnhaus  21961  hauscmplem  22013  fsubbas  22474  metn0  22969  nmne0  23227  nmgt0  23238  iccpnfhmeo  23548  ncvs1  23760  ipcau2  23836  dvcnvlem  24572  dvlip  24589  ftc1lem5  24636  mdegldg  24659  ply1divmo  24728  ig1peu  24764  ig1pdvds  24769  dgrmul  24859  coecj  24867  plydivlem4  24884  vieta1lem2  24899  vieta1  24900  aareccl  24914  geolim3  24927  abelthlem2  25019  abelthlem7  25025  tanregt0  25122  tanarg  25201  logtayl  25242  abscxp2  25275  cxpsqrt  25285  abscxpbnd  25333  logrec  25340  ang180lem1  25386  ang180lem2  25387  ang180lem3  25388  lawcos  25393  isosctr  25398  asinlem  25445  atandm2  25454  atandm4  25456  2efiatan  25495  tanatan  25496  atandmtan  25497  dvatan  25512  mersenne  25802  perfectlem2  25805  dchrinv  25836  dchrptlem2  25840  dchrsum2  25843  sumdchr2  25845  lgsabs1  25911  dchrisum0re  26088  tgcgrneq  26268  footexALT  26503  footexlem1  26504  footexlem2  26505  colinearalg  26695  axsegconlem6  26707  axsegconlem9  26710  ax5seglem5  26718  axlowdimlem14  26740  wlkn0  27401  cyclnspth  27580  iswwlksnx  27617  wwlksm1edg  27658  wspthsnonn0vne  27695  umgrclwwlkge2  27768  clwwisshclwws  27792  hashecclwwlkn1  27855  umgrhashecclwwlk  27856  frgrregord013  28173  frgrogt3nreg  28175  friendshipgt3  28176  nvgt0  28450  nv1  28451  nmlnogt0  28573  nmblolbii  28575  blocnilem  28580  normne0  28906  normcan  29352  nmlnopne0  29775  nmophmi  29807  riesz3i  29838  ogrpsublt  30722  cycpmco2lem6  30773  esumpcvgval  31337  ballotlemfrcn0  31787  signsply0  31821  signstfvn  31839  signsvtn0  31840  signstfvneq0  31842  signstfveq0a  31846  signshnz  31861  bnj168  32000  usgrgt2cycl  32377  erdszelem9  32446  sltval2  33163  segcon2  33566  outsideofeu  33592  heicant  34926  smprngopr  35329  isfldidl2  35346  isdmn3  35351  lsat0cv  36168  lcvexchlem1  36169  lsatcvat2  36186  lkrshp  36240  lkrshp3  36241  lkrpssN  36298  cvrat2  36564  atcvrneN  36565  atcvrj2b  36567  2llnmat  36659  2lnat  36919  pmapjat1  36988  pclfinclN  37085  lautlt  37226  ltrn11at  37282  ltrnatneq  37317  trlcone  37863  tendoconid  37964  tendotr  37965  cdleml3N  38113  dochsordN  38509  dochn0nv  38510  djhcvat42  38550  dochsatshp  38586  lcfl8b  38639  lclkrlem2a  38642  lcfrlem9  38685  mapdsord  38790  mapdncol  38805  mapdpglem29  38835  mapdindp1  38855  hdmapnzcl  38980  hdmaprnlem1N  38984  hdmaprnlem3N  38985  hdmaprnlem3uN  38986  hdmaprnlem9N  38992  hdmap14lem9  39011  hgmapval1  39028  hgmapadd  39029  hgmapmul  39030  hgmaprnlem1N  39031  hdmaplkr  39048  hdmapip1  39051  hgmapvvlem1  39058  hgmapvvlem2  39059  hgmapvvlem3  39060  jm2.19  39588  jm2.26lem3  39596  kelac1  39661  mpaaeu  39748  radcnvrat  40644  binomcxplemnotnn0  40686  sqrtnegnre  43506  paireqne  43672  fmtnoprmfac1lem  43725  requad01  43785  requad2  43787  perfectALTVlem2  43886  nnsgrpnmnd  44084  rrx2pnedifcoorneor  44702  rrx2pnedifcoorneorr  44703  eenglngeehlnmlem2  44724  onetansqsecsq  44859