Theorem necon3bid 3008

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

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

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 2965

This theorem is referenced by:  neeq1d  3023  neeq2d  3024  neeq12d  3025  nebi  3044  pr1nebg  4827  f1dom3fv3dif  7267  frxp  8121  frxp2  8139  frxp3  8146  suppval1  8161  iinon  8326  fodomfib  9287  wemapso  9512  wemapso2lem  9513  infpssrlem4  10289  ttukeylem6  10497  fodomb  10509  tskcard  10765  addneintrd  11416  addneintr2d  11417  negne0bd  11561  negned  11565  subne0d  11577  subne0ad  11579  subneintrd  11612  subneintr2d  11614  divne0b  11882  div2neg  11937  divne1d  12001  div2sub  12039  xaddass2  13275  xadddi2  13322  seqf1olem1  14076  expne0  14128  sqne0  14158  hashneq0  14399  hashnncl  14401  hashgt0  14423  ccat1st1st  14665  pfxn0  14723  cjne0  15213  recval  15373  absgt0  15375  abs1m  15386  abslem2  15390  sqreulem  15410  sqreu  15411  absne0d  15500  geoserg  15919  geolim  15923  geolim2  15924  georeclim  15925  geoisum1c  15933  tanval2  16188  tanaddlem  16221  tanadd  16222  4sqlem11  17014  ipodrsima  18596  chnind  18676  chnub  18677  f1omvdmvd  19512  f1omvdcnv  19513  f1omvdconj  19515  pmtrfmvdn0  19531  sylow1lem4  19670  dprdf1o  20103  dprd2da  20113  ogrpsublt  20211  ringinvnz1ne0  20382  rrgsupp  20785  abvne0  20899  gzrngunit  21551  chrnzr  21648  obsne0  21843  mdetdiaglem  22723  cnhaus  23479  hauscmplem  23531  fsubbas  23992  metn0  24485  nmne0  24744  nmgt0  24755  iccpnfhmeo  25072  ncvs1  25284  ipcau2  25361  dvcnvlem  26103  dvlip  26120  ftc1lem5  26167  mdegldg  26191  ply1divmo  26261  ig1peu  26300  ig1pdvds  26305  dgrmul  26395  coecj  26403  coecjOLD  26405  plydivlem4  26425  vieta1lem2  26440  vieta1  26441  aareccl  26455  geolim3  26468  abelthlem2  26560  abelthlem7  26566  tanregt0  26669  tanarg  26749  logtayl  26790  abscxp2  26823  cxpsqrt  26833  abscxpbnd  26883  logrec  26893  ang180lem1  26939  ang180lem2  26940  ang180lem3  26941  lawcos  26946  isosctr  26951  asinlem  26998  atandm2  27007  atandm4  27009  2efiatan  27048  tanatan  27049  atandmtan  27050  dvatan  27065  mersenne  27356  perfectlem2  27359  dchrinv  27390  dchrptlem2  27394  dchrsum2  27397  sumdchr2  27399  lgsabs1  27465  dchrisum0re  27642  ltsval2  27785  bday1  27972  cuteq1  27975  n0subs2  28522  tgcgrneq  28717  footexALT  28956  footexlem1  28957  footexlem2  28958  colinearalg  29200  axsegconlem6  29212  axsegconlem9  29215  ax5seglem5  29223  axlowdimlem14  29245  wlkn0  29910  cyclnspth  30090  iswwlksnx  30129  wwlksm1edg  30170  wspthsnonn0vne  30206  umgrclwwlkge2  30282  clwwisshclwws  30306  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  frgrregord013  30686  frgrogt3nreg  30688  friendshipgt3  30689  nrt2irr  30764  nvgt0  30966  nv1  30967  nmlnogt0  31089  nmblolbii  31091  blocnilem  31096  normne0  31422  normcan  31868  nmlnopne0  32291  nmophmi  32323  riesz3i  32354  hashne0  33094  wrdpmtrlast  33353  cycpmco2lem6  33391  1arithidom  33771  ply1unit  33809  m1pmeq  33819  minplyirredlem  34044  constrrtcclem  34068  constrconj  34079  iconstr  34100  zarclssn  34207  esumpcvgval  34412  ballotlemfrcn0  34864  signsply0  34882  signstfvn  34900  signsvtn0  34901  signstfvneq0  34903  signstfveq0a  34907  signshnz  34922  bnj168  35063  nummin  35426  usgrgt2cycl  35520  erdszelem9  35589  segcon2  36495  outsideofeu  36521  heicant  38193  smprngopr  38590  isfldidl2  38607  isdmn3  38612  lsat0cv  39696  lcvexchlem1  39697  lsatcvat2  39714  lkrshp  39768  lkrshp3  39769  lkrpssN  39826  cvrat2  40092  atcvrneN  40093  atcvrj2b  40095  2llnmat  40187  2lnat  40447  pmapjat1  40516  pclfinclN  40613  lautlt  40754  ltrn11at  40810  ltrnatneq  40845  trlcone  41391  tendoconid  41492  tendotr  41493  cdleml3N  41641  dochsordN  42037  dochn0nv  42038  djhcvat42  42078  dochsatshp  42114  lcfl8b  42167  lclkrlem2a  42170  lcfrlem9  42213  mapdsord  42318  mapdncol  42333  mapdpglem29  42363  mapdindp1  42383  hdmapnzcl  42508  hdmaprnlem1N  42512  hdmaprnlem3N  42513  hdmaprnlem3uN  42514  hdmaprnlem9N  42520  hdmap14lem9  42539  hgmapval1  42556  hgmapadd  42557  hgmapmul  42558  hgmaprnlem1N  42559  hdmaplkr  42576  hdmapip1  42579  hgmapvvlem1  42586  hgmapvvlem2  42587  hgmapvvlem3  42588  fldhmf1  42746  aks6d1c2p2  42775  aks6d1c5lem2  42794  aks6d1c6lem3  42828  redivne0bd  43100  fsuppind  43213  jm2.19  43611  jm2.26lem3  43619  kelac1  43681  mpaaeu  43768  radcnvrat  44915  binomcxplemnotnn0  44957  sqrtnegnre  47932  paireqne  48148  fmtnoprmfac1lem  48204  requad01  48274  requad2  48276  perfectALTVlem2  48375  nnsgrpnmnd  48831  rrx2pnedifcoorneor  49380  rrx2pnedifcoorneorr  49381  eenglngeehlnmlem2  49402  fdomne0  49512  oppcendc  49680  onetansqsecsq  50423