Theorem necon3bid 3003

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  neeq1d  3018  neeq2d  3019  neeq12d  3020  nebi  3039  pr1nebg  4818  f1dom3fv3dif  7303  frxp  8175  fnwe2lem3  8184  frxp2  8198  frxp3  8205  suppval1  8221  iinon  8386  onelfvnef1  8487  fodomfib  9358  wemapso  9582  wemapso2lem  9583  infpssrlem4  10423  ttukeylem6  10631  fodomb  10644  tskcard  10905  addneintrd  11556  addneintr2d  11557  negne0bd  11701  negned  11705  subne0d  11718  subne0ad  11719  subneintrd  11752  subneintr2d  11754  divne0b  12025  div2neg  12080  divne1d  12144  div2sub  12182  xaddass2  13420  xadddi2  13467  seqf1olem1  14224  expne0  14276  sqne0  14306  hashneq0  14549  hashnncl  14551  hashgt0  14573  ccat1st1st  14818  pfxn0  14878  cjne0  15373  recval  15533  absgt0  15535  abs1m  15546  abslem2  15551  sqreulem  15571  sqreu  15572  absne0d  15661  geoserg  16079  geolim  16083  geolim2  16084  georeclim  16085  geoisum1c  16093  tanval2  16345  tanaddlem  16378  tanadd  16379  4sqlem11  17177  ipodrsima  18765  chnind  18845  chnub  18846  f1omvdmvd  19708  f1omvdcnv  19709  f1omvdconj  19711  pmtrfmvdn0  19727  sylow1lem4  19866  dprdf1o  20299  dprd2da  20309  ogrpsublt  20407  ringinvnz1ne0  20582  rrgsupp  21004  abvne0  21127  isfieldidl2  21592  gzrngunit  21793  chrnzr  21891  obsne0  22086  mdetdiaglem  22968  cnhaus  23727  hauscmplem  23779  fsubbas  24241  metn0  24734  nmne0  24993  nmgt0  25004  iccpnfhmeo  25321  ncvs1  25533  ipcau2  25610  dvcnvlem  26351  dvlip  26368  ftc1lem5  26415  mdegldg  26439  ply1divmo  26509  ig1peu  26548  ig1pdvds  26553  dgrmul  26644  coecj  26652  plydivlem4  26672  rnplynfin  26685  vieta1lem2  26689  vieta1  26690  aareccl  26710  geolim3  26723  abelthlem2  26816  abelthlem7  26822  tanregt0  26924  tanarg  27004  logtayl  27045  abscxp2  27078  cxpsqrt  27088  abscxpbnd  27138  logrec  27148  ang180lem1  27194  ang180lem2  27195  ang180lem3  27196  lawcos  27201  isosctr  27206  asinlem  27253  atandm2  27262  atandm4  27264  2efiatan  27303  tanatan  27304  atandmtan  27305  dvatan  27320  mersenne  27611  perfectlem2  27614  dchrinv  27645  dchrptlem2  27649  dchrsum2  27652  sumdchr2  27654  lgsabs1  27720  dchrisum0re  27897  ltsval2  28070  bday1  28257  cuteq1  28260  n0subs2  28807  tgcgrneq  29002  mirlni  29224  footexALT  29250  footexlem1  29251  footexlem2  29252  prlngsymquadlem  29498  colinearalg  29545  axsegconlem6  29557  axsegconlem9  29560  ax5seglem5  29568  axlowdimlem14  29590  wlkn0  30258  cyclnspth  30446  iswwlksnx  30486  wwlksm1edg  30527  wspthsnonn0vne  30563  umgrclwwlkge2  30639  clwwisshclwws  30663  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  frgrregord013  31053  frgrogt3nreg  31055  friendshipgt3  31056  nrt2irr  31131  nvgt0  31333  nv1  31334  nmlnogt0  31456  nmblolbii  31458  blocnilem  31463  normne0  31789  normcan  32235  nmlnopne0  32658  nmophmi  32690  riesz3i  32721  tgextamirnhl  33129  hashne0  33497  wrdpmtrlast  33753  cycpmco2lem6  33791  1arithidom  34173  ply1unit  34210  m1pmeq  34220  minplyirredlem  34453  constrrtcclem  34477  constrconj  34488  iconstr  34509  zarclssn  34616  esumpcvgval  34821  ballotlemfrcn0  35273  signsply0  35291  signstfvn  35309  signsvtn0  35310  signstfvneq0  35312  signstfveq0a  35316  signshnz  35331  bnj168  35472  nummin  35847  usgrgt2cycl  36107  erdszelem9  36172  segcon2  37085  outsideofeu  37111  mh-inf3f1  37544  heicant  38841  smprngopr  39252  isfldidl2  39269  isdmn3  39274  lsat0cv  40356  lcvexchlem1  40357  lsatcvat2  40374  lkrshp  40428  lkrshp3  40429  lkrpssN  40486  cvrat2  40752  atcvrneN  40753  atcvrj2b  40755  2llnmat  40847  2lnat  41107  pmapjat1  41176  pclfinclN  41273  lautlt  41414  ltrn11at  41470  ltrnatneq  41505  trlcone  42051  tendoconid  42152  tendotr  42153  cdleml3N  42301  dochsordN  42697  dochn0nv  42698  djhcvat42  42738  dochsatshp  42774  lcfl8b  42827  lclkrlem2a  42830  lcfrlem9  42873  mapdsord  42978  mapdncol  42993  mapdpglem29  43023  mapdindp1  43043  hdmapnzcl  43168  hdmaprnlem1N  43172  hdmaprnlem3N  43173  hdmaprnlem3uN  43174  hdmaprnlem9N  43180  hdmap14lem9  43199  hgmapval1  43216  hgmapadd  43217  hgmapmul  43218  hgmaprnlem1N  43219  hdmaplkr  43236  hdmapip1  43239  hgmapvvlem1  43246  hgmapvvlem2  43247  hgmapvvlem3  43248  fldhmf1  43406  aks6d1c2p2  43435  aks6d1c5lem2  43454  aks6d1c6lem3  43488  redivne0bd  43767  fsuppind  43884  frlmnzcoordsca  43924  jm2.19  44266  jm2.26lem3  44274  kelac1  44331  mpaaeu  44417  radcnvrat  45559  binomcxplemnotnn0  45601  sqrtnegnre  48650  paireqne  48866  fmtnoprmfac1lem  48922  requad01  48992  requad2  48994  perfectALTVlem2  49093  nnsgrpnmnd  49548  isidom3  49773  rrx2pnedifcoorneor  50160  rrx2pnedifcoorneorr  50161  eenglngeehlnmlem2  50182  fdomne0  50292  oppcendc  50463  onetansqsecsq  51282