Theorem necon3bid 2983

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

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

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 2939

This theorem is referenced by:  neeq1d  2998  neeq2d  2999  neeq12d  3000  nebi  3019  pr1nebg  4857  f1dom3fv3dif  7269  frxp  8114  frxp2  8132  frxp3  8139  suppval1  8154  iinon  8342  fodomfib  9328  wemapso  9548  wemapso2lem  9549  infpssrlem4  10303  ttukeylem6  10511  fodomb  10523  tskcard  10778  addneintrd  11425  addneintr2d  11426  negne0bd  11568  negned  11572  subne0d  11584  subne0ad  11586  subneintrd  11619  subneintr2d  11621  divne0b  11887  div2neg  11941  divne1d  12005  div2sub  12043  xaddass2  13233  xadddi2  13280  seqf1olem1  14011  expne0  14063  sqne0  14092  hashneq0  14328  hashnncl  14330  hashgt0  14352  ccat1st1st  14582  pfxn0  14640  cjne0  15114  recval  15273  absgt0  15275  abs1m  15286  abslem2  15290  sqreulem  15310  sqreu  15311  absne0d  15398  geoserg  15816  geolim  15820  geolim2  15821  georeclim  15822  geoisum1c  15830  tanval2  16080  tanaddlem  16113  tanadd  16114  4sqlem11  16892  ipodrsima  18498  f1omvdmvd  19352  f1omvdcnv  19353  f1omvdconj  19355  pmtrfmvdn0  19371  sylow1lem4  19510  dprdf1o  19943  dprd2da  19953  ringinvnz1ne0  20188  abvne0  20578  rrgsupp  21107  gzrngunit  21211  chrnzr  21301  obsne0  21499  mdetdiaglem  22320  cnhaus  23078  hauscmplem  23130  fsubbas  23591  metn0  24086  nmne0  24348  nmgt0  24359  iccpnfhmeo  24690  ncvs1  24905  ipcau2  24982  dvcnvlem  25728  dvlip  25745  ftc1lem5  25792  mdegldg  25819  ply1divmo  25888  ig1peu  25924  ig1pdvds  25929  dgrmul  26020  coecj  26028  plydivlem4  26045  vieta1lem2  26060  vieta1  26061  aareccl  26075  geolim3  26088  abelthlem2  26180  abelthlem7  26186  tanregt0  26284  tanarg  26363  logtayl  26404  abscxp2  26437  cxpsqrt  26447  abscxpbnd  26497  logrec  26504  ang180lem1  26550  ang180lem2  26551  ang180lem3  26552  lawcos  26557  isosctr  26562  asinlem  26609  atandm2  26618  atandm4  26620  2efiatan  26659  tanatan  26660  atandmtan  26661  dvatan  26676  mersenne  26966  perfectlem2  26969  dchrinv  27000  dchrptlem2  27004  dchrsum2  27007  sumdchr2  27009  lgsabs1  27075  dchrisum0re  27252  sltval2  27395  bday1s  27569  cuteq1  27571  tgcgrneq  28001  footexALT  28236  footexlem1  28237  footexlem2  28238  colinearalg  28435  axsegconlem6  28447  axsegconlem9  28450  ax5seglem5  28458  axlowdimlem14  28480  wlkn0  29145  cyclnspth  29324  iswwlksnx  29361  wwlksm1edg  29402  wspthsnonn0vne  29438  umgrclwwlkge2  29511  clwwisshclwws  29535  hashecclwwlkn1  29597  umgrhashecclwwlk  29598  frgrregord013  29915  frgrogt3nreg  29917  friendshipgt3  29918  nrt2irr  29993  nvgt0  30194  nv1  30195  nmlnogt0  30317  nmblolbii  30319  blocnilem  30324  normne0  30650  normcan  31096  nmlnopne0  31519  nmophmi  31551  riesz3i  31582  ogrpsublt  32509  cycpmco2lem6  32560  minplyirredlem  33058  zarclssn  33151  esumpcvgval  33374  ballotlemfrcn0  33826  signsply0  33860  signstfvn  33878  signsvtn0  33879  signstfvneq0  33881  signstfveq0a  33885  signshnz  33900  bnj168  34039  nummin  34392  usgrgt2cycl  34419  erdszelem9  34488  segcon2  35381  outsideofeu  35407  heicant  36826  smprngopr  37223  isfldidl2  37240  isdmn3  37245  lsat0cv  38206  lcvexchlem1  38207  lsatcvat2  38224  lkrshp  38278  lkrshp3  38279  lkrpssN  38336  cvrat2  38603  atcvrneN  38604  atcvrj2b  38606  2llnmat  38698  2lnat  38958  pmapjat1  39027  pclfinclN  39124  lautlt  39265  ltrn11at  39321  ltrnatneq  39356  trlcone  39902  tendoconid  40003  tendotr  40004  cdleml3N  40152  dochsordN  40548  dochn0nv  40549  djhcvat42  40589  dochsatshp  40625  lcfl8b  40678  lclkrlem2a  40681  lcfrlem9  40724  mapdsord  40829  mapdncol  40844  mapdpglem29  40874  mapdindp1  40894  hdmapnzcl  41019  hdmaprnlem1N  41023  hdmaprnlem3N  41024  hdmaprnlem3uN  41025  hdmaprnlem9N  41031  hdmap14lem9  41050  hgmapval1  41067  hgmapadd  41068  hgmapmul  41069  hgmaprnlem1N  41070  hdmaplkr  41087  hdmapip1  41090  hgmapvvlem1  41097  hgmapvvlem2  41098  hgmapvvlem3  41099  fldhmf1  41261  aks6d1c2p2  41263  fsuppind  41464  jm2.19  42034  jm2.26lem3  42042  kelac1  42107  mpaaeu  42194  radcnvrat  43375  binomcxplemnotnn0  43417  sqrtnegnre  46313  paireqne  46477  fmtnoprmfac1lem  46530  requad01  46587  requad2  46589  perfectALTVlem2  46688  nnsgrpnmnd  46854  rrx2pnedifcoorneor  47489  rrx2pnedifcoorneorr  47490  eenglngeehlnmlem2  47511  fdomne0  47603  onetansqsecsq  47893