Theorem necon3bid 2987

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 2943	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 2980	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	syl5bb 282	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  neeq1d  3002  neeq2d  3003  neeq12d  3004  nebi  3023  pr1nebg  4785  f1dom3fv3dif  7122  frxp  7938  suppval1  7954  iinon  8142  fodomfib  9023  wemapso  9240  wemapso2lem  9241  infpssrlem4  9993  ttukeylem6  10201  fodomb  10213  tskcard  10468  addneintrd  11112  addneintr2d  11113  negne0bd  11255  negned  11259  subne0d  11271  subne0ad  11273  subneintrd  11306  subneintr2d  11308  divne0b  11574  div2neg  11628  divne1d  11692  div2sub  11730  xaddass2  12913  xadddi2  12960  seqf1olem1  13690  expne0  13742  sqne0  13771  hashneq0  14007  hashnncl  14009  hashgt0  14031  ccat1st1st  14263  pfxn0  14327  cjne0  14802  recval  14962  absgt0  14964  abs1m  14975  abslem2  14979  sqreulem  14999  sqreu  15000  absne0d  15087  geoserg  15506  geolim  15510  geolim2  15511  georeclim  15512  geoisum1c  15520  tanval2  15770  tanaddlem  15803  tanadd  15804  4sqlem11  16584  ipodrsima  18174  f1omvdmvd  18966  f1omvdcnv  18967  f1omvdconj  18969  pmtrfmvdn0  18985  sylow1lem4  19121  dprdf1o  19550  dprd2da  19560  ringinvnz1ne0  19746  abvne0  20002  rrgsupp  20475  gzrngunit  20576  chrnzr  20646  obsne0  20842  mdetdiaglem  21655  cnhaus  22413  hauscmplem  22465  fsubbas  22926  metn0  23421  nmne0  23681  nmgt0  23692  iccpnfhmeo  24014  ncvs1  24226  ipcau2  24303  dvcnvlem  25045  dvlip  25062  ftc1lem5  25109  mdegldg  25136  ply1divmo  25205  ig1peu  25241  ig1pdvds  25246  dgrmul  25336  coecj  25344  plydivlem4  25361  vieta1lem2  25376  vieta1  25377  aareccl  25391  geolim3  25404  abelthlem2  25496  abelthlem7  25502  tanregt0  25600  tanarg  25679  logtayl  25720  abscxp2  25753  cxpsqrt  25763  abscxpbnd  25811  logrec  25818  ang180lem1  25864  ang180lem2  25865  ang180lem3  25866  lawcos  25871  isosctr  25876  asinlem  25923  atandm2  25932  atandm4  25934  2efiatan  25973  tanatan  25974  atandmtan  25975  dvatan  25990  mersenne  26280  perfectlem2  26283  dchrinv  26314  dchrptlem2  26318  dchrsum2  26321  sumdchr2  26323  lgsabs1  26389  dchrisum0re  26566  tgcgrneq  26748  footexALT  26983  footexlem1  26984  footexlem2  26985  colinearalg  27181  axsegconlem6  27193  axsegconlem9  27196  ax5seglem5  27204  axlowdimlem14  27226  wlkn0  27890  cyclnspth  28069  iswwlksnx  28106  wwlksm1edg  28147  wspthsnonn0vne  28183  umgrclwwlkge2  28256  clwwisshclwws  28280  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  frgrregord013  28660  frgrogt3nreg  28662  friendshipgt3  28663  nvgt0  28937  nv1  28938  nmlnogt0  29060  nmblolbii  29062  blocnilem  29067  normne0  29393  normcan  29839  nmlnopne0  30262  nmophmi  30294  riesz3i  30325  ogrpsublt  31249  cycpmco2lem6  31300  zarclssn  31725  esumpcvgval  31946  ballotlemfrcn0  32396  signsply0  32430  signstfvn  32448  signsvtn0  32449  signstfvneq0  32451  signstfveq0a  32455  signshnz  32470  bnj168  32609  nummin  32963  usgrgt2cycl  32992  erdszelem9  33061  frxp2  33718  frxp3  33724  sltval2  33786  bday1s  33952  segcon2  34334  outsideofeu  34360  heicant  35739  smprngopr  36137  isfldidl2  36154  isdmn3  36159  lsat0cv  36974  lcvexchlem1  36975  lsatcvat2  36992  lkrshp  37046  lkrshp3  37047  lkrpssN  37104  cvrat2  37370  atcvrneN  37371  atcvrj2b  37373  2llnmat  37465  2lnat  37725  pmapjat1  37794  pclfinclN  37891  lautlt  38032  ltrn11at  38088  ltrnatneq  38123  trlcone  38669  tendoconid  38770  tendotr  38771  cdleml3N  38919  dochsordN  39315  dochn0nv  39316  djhcvat42  39356  dochsatshp  39392  lcfl8b  39445  lclkrlem2a  39448  lcfrlem9  39491  mapdsord  39596  mapdncol  39611  mapdpglem29  39641  mapdindp1  39661  hdmapnzcl  39786  hdmaprnlem1N  39790  hdmaprnlem3N  39791  hdmaprnlem3uN  39792  hdmaprnlem9N  39798  hdmap14lem9  39817  hgmapval1  39834  hgmapadd  39835  hgmapmul  39836  hgmaprnlem1N  39837  hdmaplkr  39854  hdmapip1  39857  hgmapvvlem1  39864  hgmapvvlem2  39865  hgmapvvlem3  39866  fsuppind  40202  jm2.19  40731  jm2.26lem3  40739  kelac1  40804  mpaaeu  40891  radcnvrat  41821  binomcxplemnotnn0  41863  sqrtnegnre  44687  paireqne  44851  fmtnoprmfac1lem  44904  requad01  44961  requad2  44963  perfectALTVlem2  45062  nnsgrpnmnd  45260  rrx2pnedifcoorneor  45950  rrx2pnedifcoorneorr  45951  eenglngeehlnmlem2  45972  fdomne0  46065  onetansqsecsq  46349