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  4818  f1dom3fv3dif  7225  frxp  8082  frxp2  8100  frxp3  8107  suppval1  8122  iinon  8286  fodomfib  9256  fodomfibOLD  9258  wemapso  9480  wemapso2lem  9481  infpssrlem4  10235  ttukeylem6  10443  fodomb  10455  tskcard  10710  addneintrd  11357  addneintr2d  11358  negne0bd  11502  negned  11506  subne0d  11518  subne0ad  11520  subneintrd  11553  subneintr2d  11555  divne0b  11824  div2neg  11881  divne1d  11945  div2sub  11983  xaddass2  13186  xadddi2  13233  seqf1olem1  13982  expne0  14034  sqne0  14064  hashneq0  14305  hashnncl  14307  hashgt0  14329  ccat1st1st  14569  pfxn0  14627  cjne0  15105  recval  15265  absgt0  15267  abs1m  15278  abslem2  15282  sqreulem  15302  sqreu  15303  absne0d  15392  geoserg  15808  geolim  15812  geolim2  15813  georeclim  15814  geoisum1c  15822  tanval2  16077  tanaddlem  16110  tanadd  16111  4sqlem11  16902  ipodrsima  18482  f1omvdmvd  19357  f1omvdcnv  19358  f1omvdconj  19360  pmtrfmvdn0  19376  sylow1lem4  19515  dprdf1o  19948  dprd2da  19958  ogrpsublt  20056  ringinvnz1ne0  20220  rrgsupp  20621  abvne0  20739  gzrngunit  21375  chrnzr  21472  obsne0  21667  mdetdiaglem  22518  cnhaus  23274  hauscmplem  23326  fsubbas  23787  metn0  24281  nmne0  24540  nmgt0  24551  iccpnfhmeo  24876  ncvs1  25090  ipcau2  25167  dvcnvlem  25913  dvlip  25931  ftc1lem5  25980  mdegldg  26004  ply1divmo  26074  ig1peu  26113  ig1pdvds  26118  dgrmul  26209  coecj  26217  coecjOLD  26219  plydivlem4  26237  vieta1lem2  26252  vieta1  26253  aareccl  26267  geolim3  26280  abelthlem2  26375  abelthlem7  26381  tanregt0  26481  tanarg  26561  logtayl  26602  abscxp2  26635  cxpsqrt  26645  abscxpbnd  26696  logrec  26706  ang180lem1  26752  ang180lem2  26753  ang180lem3  26754  lawcos  26759  isosctr  26764  asinlem  26811  atandm2  26820  atandm4  26822  2efiatan  26861  tanatan  26862  atandmtan  26863  dvatan  26878  mersenne  27171  perfectlem2  27174  dchrinv  27205  dchrptlem2  27209  dchrsum2  27212  sumdchr2  27214  lgsabs1  27280  dchrisum0re  27457  sltval2  27601  bday1s  27780  cuteq1  27783  n0subs2  28294  tgcgrneq  28463  footexALT  28698  footexlem1  28699  footexlem2  28700  colinearalg  28890  axsegconlem6  28902  axsegconlem9  28905  ax5seglem5  28913  axlowdimlem14  28935  wlkn0  29601  cyclnspth  29781  iswwlksnx  29820  wwlksm1edg  29861  wspthsnonn0vne  29897  umgrclwwlkge2  29970  clwwisshclwws  29994  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  frgrregord013  30374  frgrogt3nreg  30376  friendshipgt3  30377  nrt2irr  30452  nvgt0  30653  nv1  30654  nmlnogt0  30776  nmblolbii  30778  blocnilem  30783  normne0  31109  normcan  31555  nmlnopne0  31978  nmophmi  32010  riesz3i  32041  hashne0  32785  chnind  32983  chnub  32984  wrdpmtrlast  33065  cycpmco2lem6  33103  1arithidom  33501  ply1unit  33537  m1pmeq  33545  minplyirredlem  33693  constrrtcclem  33717  constrconj  33728  iconstr  33749  zarclssn  33856  esumpcvgval  34061  ballotlemfrcn0  34514  signsply0  34535  signstfvn  34553  signsvtn0  34554  signstfvneq0  34556  signstfveq0a  34560  signshnz  34575  bnj168  34713  nummin  35074  usgrgt2cycl  35110  erdszelem9  35179  segcon2  36086  outsideofeu  36112  heicant  37642  smprngopr  38039  isfldidl2  38056  isdmn3  38061  lsat0cv  39019  lcvexchlem1  39020  lsatcvat2  39037  lkrshp  39091  lkrshp3  39092  lkrpssN  39149  cvrat2  39416  atcvrneN  39417  atcvrj2b  39419  2llnmat  39511  2lnat  39771  pmapjat1  39840  pclfinclN  39937  lautlt  40078  ltrn11at  40134  ltrnatneq  40169  trlcone  40715  tendoconid  40816  tendotr  40817  cdleml3N  40965  dochsordN  41361  dochn0nv  41362  djhcvat42  41402  dochsatshp  41438  lcfl8b  41491  lclkrlem2a  41494  lcfrlem9  41537  mapdsord  41642  mapdncol  41657  mapdpglem29  41687  mapdindp1  41707  hdmapnzcl  41832  hdmaprnlem1N  41836  hdmaprnlem3N  41837  hdmaprnlem3uN  41838  hdmaprnlem9N  41844  hdmap14lem9  41863  hgmapval1  41880  hgmapadd  41881  hgmapmul  41882  hgmaprnlem1N  41883  hdmaplkr  41900  hdmapip1  41903  hgmapvvlem1  41910  hgmapvvlem2  41911  hgmapvvlem3  41912  fldhmf1  42071  aks6d1c2p2  42100  aks6d1c5lem2  42119  aks6d1c6lem3  42153  fsuppind  42571  jm2.19  42975  jm2.26lem3  42983  kelac1  43045  mpaaeu  43132  radcnvrat  44296  binomcxplemnotnn0  44338  sqrtnegnre  47301  paireqne  47505  fmtnoprmfac1lem  47558  requad01  47615  requad2  47617  perfectALTVlem2  47716  nnsgrpnmnd  48159  rrx2pnedifcoorneor  48698  rrx2pnedifcoorneorr  48699  eenglngeehlnmlem2  48720  fdomne0  48831  oppcendc  49000  onetansqsecsq  49743