Theorem necon3bid 2969

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

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

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 2926

This theorem is referenced by:  neeq1d  2984  neeq2d  2985  neeq12d  2986  nebi  3005  pr1nebg  4809  f1dom3fv3dif  7205  frxp  8059  frxp2  8077  frxp3  8084  suppval1  8099  iinon  8263  fodomfib  9219  fodomfibOLD  9221  wemapso  9443  wemapso2lem  9444  infpssrlem4  10200  ttukeylem6  10408  fodomb  10420  tskcard  10675  addneintrd  11323  addneintr2d  11324  negne0bd  11468  negned  11472  subne0d  11484  subne0ad  11486  subneintrd  11519  subneintr2d  11521  divne0b  11790  div2neg  11847  divne1d  11911  div2sub  11949  xaddass2  13152  xadddi2  13199  seqf1olem1  13948  expne0  14000  sqne0  14030  hashneq0  14271  hashnncl  14273  hashgt0  14295  ccat1st1st  14535  pfxn0  14593  cjne0  15070  recval  15230  absgt0  15232  abs1m  15243  abslem2  15247  sqreulem  15267  sqreu  15268  absne0d  15357  geoserg  15773  geolim  15777  geolim2  15778  georeclim  15779  geoisum1c  15787  tanval2  16042  tanaddlem  16075  tanadd  16076  4sqlem11  16867  ipodrsima  18447  f1omvdmvd  19322  f1omvdcnv  19323  f1omvdconj  19325  pmtrfmvdn0  19341  sylow1lem4  19480  dprdf1o  19913  dprd2da  19923  ogrpsublt  20021  ringinvnz1ne0  20185  rrgsupp  20586  abvne0  20704  gzrngunit  21340  chrnzr  21437  obsne0  21632  mdetdiaglem  22483  cnhaus  23239  hauscmplem  23291  fsubbas  23752  metn0  24246  nmne0  24505  nmgt0  24516  iccpnfhmeo  24841  ncvs1  25055  ipcau2  25132  dvcnvlem  25878  dvlip  25896  ftc1lem5  25945  mdegldg  25969  ply1divmo  26039  ig1peu  26078  ig1pdvds  26083  dgrmul  26174  coecj  26182  coecjOLD  26184  plydivlem4  26202  vieta1lem2  26217  vieta1  26218  aareccl  26232  geolim3  26245  abelthlem2  26340  abelthlem7  26346  tanregt0  26446  tanarg  26526  logtayl  26567  abscxp2  26600  cxpsqrt  26610  abscxpbnd  26661  logrec  26671  ang180lem1  26717  ang180lem2  26718  ang180lem3  26719  lawcos  26724  isosctr  26729  asinlem  26776  atandm2  26785  atandm4  26787  2efiatan  26826  tanatan  26827  atandmtan  26828  dvatan  26843  mersenne  27136  perfectlem2  27139  dchrinv  27170  dchrptlem2  27174  dchrsum2  27177  sumdchr2  27179  lgsabs1  27245  dchrisum0re  27422  sltval2  27566  bday1s  27745  cuteq1  27748  n0subs2  28259  tgcgrneq  28428  footexALT  28663  footexlem1  28664  footexlem2  28665  colinearalg  28855  axsegconlem6  28867  axsegconlem9  28870  ax5seglem5  28878  axlowdimlem14  28900  wlkn0  29566  cyclnspth  29746  iswwlksnx  29785  wwlksm1edg  29826  wspthsnonn0vne  29862  umgrclwwlkge2  29935  clwwisshclwws  29959  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  frgrregord013  30339  frgrogt3nreg  30341  friendshipgt3  30342  nrt2irr  30417  nvgt0  30618  nv1  30619  nmlnogt0  30741  nmblolbii  30743  blocnilem  30748  normne0  31074  normcan  31520  nmlnopne0  31943  nmophmi  31975  riesz3i  32006  hashne0  32755  chnind  32953  chnub  32954  wrdpmtrlast  33035  cycpmco2lem6  33073  1arithidom  33474  ply1unit  33510  m1pmeq  33519  minplyirredlem  33677  constrrtcclem  33701  constrconj  33712  iconstr  33733  zarclssn  33840  esumpcvgval  34045  ballotlemfrcn0  34498  signsply0  34519  signstfvn  34537  signsvtn0  34538  signstfvneq0  34540  signstfveq0a  34544  signshnz  34559  bnj168  34697  nummin  35058  usgrgt2cycl  35107  erdszelem9  35176  segcon2  36083  outsideofeu  36109  heicant  37639  smprngopr  38036  isfldidl2  38053  isdmn3  38058  lsat0cv  39016  lcvexchlem1  39017  lsatcvat2  39034  lkrshp  39088  lkrshp3  39089  lkrpssN  39146  cvrat2  39412  atcvrneN  39413  atcvrj2b  39415  2llnmat  39507  2lnat  39767  pmapjat1  39836  pclfinclN  39933  lautlt  40074  ltrn11at  40130  ltrnatneq  40165  trlcone  40711  tendoconid  40812  tendotr  40813  cdleml3N  40961  dochsordN  41357  dochn0nv  41358  djhcvat42  41398  dochsatshp  41434  lcfl8b  41487  lclkrlem2a  41490  lcfrlem9  41533  mapdsord  41638  mapdncol  41653  mapdpglem29  41683  mapdindp1  41703  hdmapnzcl  41828  hdmaprnlem1N  41832  hdmaprnlem3N  41833  hdmaprnlem3uN  41834  hdmaprnlem9N  41840  hdmap14lem9  41859  hgmapval1  41876  hgmapadd  41877  hgmapmul  41878  hgmaprnlem1N  41879  hdmaplkr  41896  hdmapip1  41899  hgmapvvlem1  41906  hgmapvvlem2  41907  hgmapvvlem3  41908  fldhmf1  42067  aks6d1c2p2  42096  aks6d1c5lem2  42115  aks6d1c6lem3  42149  fsuppind  42567  jm2.19  42970  jm2.26lem3  42978  kelac1  43040  mpaaeu  43127  radcnvrat  44291  binomcxplemnotnn0  44333  sqrtnegnre  47295  paireqne  47499  fmtnoprmfac1lem  47552  requad01  47609  requad2  47611  perfectALTVlem2  47710  nnsgrpnmnd  48166  rrx2pnedifcoorneor  48705  rrx2pnedifcoorneorr  48706  eenglngeehlnmlem2  48727  fdomne0  48838  oppcendc  49007  onetansqsecsq  49750