Theorem necon3bid 2977

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  neeq1d  2992  neeq2d  2993  neeq12d  2994  nebi  3013  pr1nebg  4816  f1dom3fv3dif  7224  frxp  8078  frxp2  8096  frxp3  8103  suppval1  8118  iinon  8282  fodomfib  9241  fodomfibOLD  9243  wemapso  9468  wemapso2lem  9469  infpssrlem4  10228  ttukeylem6  10436  fodomb  10448  tskcard  10704  addneintrd  11352  addneintr2d  11353  negne0bd  11497  negned  11501  subne0d  11513  subne0ad  11515  subneintrd  11548  subneintr2d  11550  divne0b  11819  div2neg  11876  divne1d  11940  div2sub  11978  xaddass2  13177  xadddi2  13224  seqf1olem1  13976  expne0  14028  sqne0  14058  hashneq0  14299  hashnncl  14301  hashgt0  14323  ccat1st1st  14564  pfxn0  14622  cjne0  15098  recval  15258  absgt0  15260  abs1m  15271  abslem2  15275  sqreulem  15295  sqreu  15296  absne0d  15385  geoserg  15801  geolim  15805  geolim2  15806  georeclim  15807  geoisum1c  15815  tanval2  16070  tanaddlem  16103  tanadd  16104  4sqlem11  16895  ipodrsima  18476  chnind  18556  chnub  18557  f1omvdmvd  19384  f1omvdcnv  19385  f1omvdconj  19387  pmtrfmvdn0  19403  sylow1lem4  19542  dprdf1o  19975  dprd2da  19985  ogrpsublt  20083  ringinvnz1ne0  20247  rrgsupp  20646  abvne0  20764  gzrngunit  21400  chrnzr  21497  obsne0  21692  mdetdiaglem  22554  cnhaus  23310  hauscmplem  23362  fsubbas  23823  metn0  24316  nmne0  24575  nmgt0  24586  iccpnfhmeo  24911  ncvs1  25125  ipcau2  25202  dvcnvlem  25948  dvlip  25966  ftc1lem5  26015  mdegldg  26039  ply1divmo  26109  ig1peu  26148  ig1pdvds  26153  dgrmul  26244  coecj  26252  coecjOLD  26254  plydivlem4  26272  vieta1lem2  26287  vieta1  26288  aareccl  26302  geolim3  26315  abelthlem2  26410  abelthlem7  26416  tanregt0  26516  tanarg  26596  logtayl  26637  abscxp2  26670  cxpsqrt  26680  abscxpbnd  26731  logrec  26741  ang180lem1  26787  ang180lem2  26788  ang180lem3  26789  lawcos  26794  isosctr  26799  asinlem  26846  atandm2  26855  atandm4  26857  2efiatan  26896  tanatan  26897  atandmtan  26898  dvatan  26913  mersenne  27206  perfectlem2  27209  dchrinv  27240  dchrptlem2  27244  dchrsum2  27247  sumdchr2  27249  lgsabs1  27315  dchrisum0re  27492  ltsval2  27636  bday1  27822  cuteq1  27825  n0subs2  28372  tgcgrneq  28567  footexALT  28802  footexlem1  28803  footexlem2  28804  colinearalg  28995  axsegconlem6  29007  axsegconlem9  29010  ax5seglem5  29018  axlowdimlem14  29040  wlkn0  29706  cyclnspth  29886  iswwlksnx  29925  wwlksm1edg  29966  wspthsnonn0vne  30002  umgrclwwlkge2  30078  clwwisshclwws  30102  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  frgrregord013  30482  frgrogt3nreg  30484  friendshipgt3  30485  nrt2irr  30560  nvgt0  30762  nv1  30763  nmlnogt0  30885  nmblolbii  30887  blocnilem  30892  normne0  31218  normcan  31664  nmlnopne0  32087  nmophmi  32119  riesz3i  32150  hashne0  32901  wrdpmtrlast  33187  cycpmco2lem6  33225  1arithidom  33630  ply1unit  33668  m1pmeq  33678  minplyirredlem  33888  constrrtcclem  33912  constrconj  33923  iconstr  33944  zarclssn  34051  esumpcvgval  34256  ballotlemfrcn0  34708  signsply0  34729  signstfvn  34747  signsvtn0  34748  signstfvneq0  34750  signstfveq0a  34754  signshnz  34769  bnj168  34907  nummin  35270  usgrgt2cycl  35346  erdszelem9  35415  segcon2  36321  outsideofeu  36347  heicant  37906  smprngopr  38303  isfldidl2  38320  isdmn3  38325  lsat0cv  39409  lcvexchlem1  39410  lsatcvat2  39427  lkrshp  39481  lkrshp3  39482  lkrpssN  39539  cvrat2  39805  atcvrneN  39806  atcvrj2b  39808  2llnmat  39900  2lnat  40160  pmapjat1  40229  pclfinclN  40326  lautlt  40467  ltrn11at  40523  ltrnatneq  40558  trlcone  41104  tendoconid  41205  tendotr  41206  cdleml3N  41354  dochsordN  41750  dochn0nv  41751  djhcvat42  41791  dochsatshp  41827  lcfl8b  41880  lclkrlem2a  41883  lcfrlem9  41926  mapdsord  42031  mapdncol  42046  mapdpglem29  42076  mapdindp1  42096  hdmapnzcl  42221  hdmaprnlem1N  42225  hdmaprnlem3N  42226  hdmaprnlem3uN  42227  hdmaprnlem9N  42233  hdmap14lem9  42252  hgmapval1  42269  hgmapadd  42270  hgmapmul  42271  hgmaprnlem1N  42272  hdmaplkr  42289  hdmapip1  42292  hgmapvvlem1  42299  hgmapvvlem2  42300  hgmapvvlem3  42301  fldhmf1  42460  aks6d1c2p2  42489  aks6d1c5lem2  42508  aks6d1c6lem3  42542  fsuppind  42948  jm2.19  43350  jm2.26lem3  43358  kelac1  43420  mpaaeu  43507  radcnvrat  44670  binomcxplemnotnn0  44712  sqrtnegnre  47667  paireqne  47871  fmtnoprmfac1lem  47924  requad01  47981  requad2  47983  perfectALTVlem2  48082  nnsgrpnmnd  48538  rrx2pnedifcoorneor  49076  rrx2pnedifcoorneorr  49077  eenglngeehlnmlem2  49098  fdomne0  49209  oppcendc  49377  onetansqsecsq  50120