Theorem necon3bid 2999

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

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

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 2956

This theorem is used by:  neeq1d  3014  neeq2d  3015  neeq12d  3016  nebi  3035  pr1nebg  4812  f1dom3fv3dif  7276  frxp  8145  fnwe2lem3  8154  frxp2  8168  frxp3  8175  suppval1  8191  iinon  8356  onelfvnef1  8457  fodomfib  9328  wemapso  9552  wemapso2lem  9553  infpssrlem4  10391  ttukeylem6  10599  fodomb  10612  tskcard  10873  addneintrd  11524  addneintr2d  11525  negne0bd  11669  negned  11673  subne0d  11686  subne0ad  11687  subneintrd  11720  subneintr2d  11722  divne0b  11992  div2neg  12047  divne1d  12111  div2sub  12149  xaddass2  13387  xadddi2  13434  seqf1olem1  14191  expne0  14243  sqne0  14273  hashneq0  14515  hashnncl  14517  hashgt0  14539  ccat1st1st  14784  pfxn0  14844  cjne0  15339  recval  15499  absgt0  15501  abs1m  15512  abslem2  15516  sqreulem  15536  sqreu  15537  absne0d  15626  geoserg  16044  geolim  16048  geolim2  16049  georeclim  16050  geoisum1c  16058  tanval2  16310  tanaddlem  16343  tanadd  16344  4sqlem11  17142  ipodrsima  18724  chnind  18804  chnub  18805  f1omvdmvd  19666  f1omvdcnv  19667  f1omvdconj  19669  pmtrfmvdn0  19685  sylow1lem4  19824  dprdf1o  20257  dprd2da  20267  ogrpsublt  20365  ringinvnz1ne0  20540  rrgsupp  20962  abvne0  21085  isfieldidl2  21550  gzrngunit  21748  chrnzr  21845  obsne0  22040  mdetdiaglem  22922  cnhaus  23681  hauscmplem  23733  fsubbas  24195  metn0  24688  nmne0  24947  nmgt0  24958  iccpnfhmeo  25275  ncvs1  25487  ipcau2  25564  dvcnvlem  26305  dvlip  26322  ftc1lem5  26369  mdegldg  26393  ply1divmo  26463  ig1peu  26502  ig1pdvds  26507  dgrmul  26598  coecj  26606  plydivlem4  26626  rnplynfin  26639  vieta1lem2  26643  vieta1  26644  aareccl  26662  geolim3  26675  abelthlem2  26768  abelthlem7  26774  tanregt0  26876  tanarg  26956  logtayl  26997  abscxp2  27030  cxpsqrt  27040  abscxpbnd  27090  logrec  27100  ang180lem1  27146  ang180lem2  27147  ang180lem3  27148  lawcos  27153  isosctr  27158  asinlem  27205  atandm2  27214  atandm4  27216  2efiatan  27255  tanatan  27256  atandmtan  27257  dvatan  27272  mersenne  27563  perfectlem2  27566  dchrinv  27597  dchrptlem2  27601  dchrsum2  27604  sumdchr2  27606  lgsabs1  27672  dchrisum0re  27849  ltsval2  28022  bday1  28209  cuteq1  28212  n0subs2  28759  tgcgrneq  28954  mirlni  29176  footexALT  29202  footexlem1  29203  footexlem2  29204  prlngsymquadlem  29450  colinearalg  29497  axsegconlem6  29509  axsegconlem9  29512  ax5seglem5  29520  axlowdimlem14  29542  wlkn0  30210  cyclnspth  30398  iswwlksnx  30438  wwlksm1edg  30479  wspthsnonn0vne  30515  umgrclwwlkge2  30591  clwwisshclwws  30615  hashecclwwlkn1  30677  umgrhashecclwwlk  30678  frgrregord013  31005  frgrogt3nreg  31007  friendshipgt3  31008  nrt2irr  31083  nvgt0  31285  nv1  31286  nmlnogt0  31408  nmblolbii  31410  blocnilem  31415  normne0  31741  normcan  32187  nmlnopne0  32610  nmophmi  32642  riesz3i  32673  tgextamirnhl  33081  hashne0  33451  wrdpmtrlast  33704  cycpmco2lem6  33742  1arithidom  34119  ply1unit  34157  m1pmeq  34167  minplyirredlem  34392  constrrtcclem  34416  constrconj  34427  iconstr  34448  zarclssn  34555  esumpcvgval  34760  ballotlemfrcn0  35212  signsply0  35230  signstfvn  35248  signsvtn0  35249  signstfvneq0  35251  signstfveq0a  35255  signshnz  35270  bnj168  35411  nummin  35780  usgrgt2cycl  36017  erdszelem9  36082  segcon2  36994  outsideofeu  37020  mh-inf3f1  37453  heicant  38710  smprngopr  39123  isfldidl2  39140  isdmn3  39145  lsat0cv  40227  lcvexchlem1  40228  lsatcvat2  40245  lkrshp  40299  lkrshp3  40300  lkrpssN  40357  cvrat2  40623  atcvrneN  40624  atcvrj2b  40626  2llnmat  40718  2lnat  40978  pmapjat1  41047  pclfinclN  41144  lautlt  41285  ltrn11at  41341  ltrnatneq  41376  trlcone  41922  tendoconid  42023  tendotr  42024  cdleml3N  42172  dochsordN  42568  dochn0nv  42569  djhcvat42  42609  dochsatshp  42645  lcfl8b  42698  lclkrlem2a  42701  lcfrlem9  42744  mapdsord  42849  mapdncol  42864  mapdpglem29  42894  mapdindp1  42914  hdmapnzcl  43039  hdmaprnlem1N  43043  hdmaprnlem3N  43044  hdmaprnlem3uN  43045  hdmaprnlem9N  43051  hdmap14lem9  43070  hgmapval1  43087  hgmapadd  43088  hgmapmul  43089  hgmaprnlem1N  43090  hdmaplkr  43107  hdmapip1  43110  hgmapvvlem1  43117  hgmapvvlem2  43118  hgmapvvlem3  43119  fldhmf1  43277  aks6d1c2p2  43306  aks6d1c5lem2  43325  aks6d1c6lem3  43359  redivne0bd  43638  fsuppind  43755  frlmnzcoordsca  43795  jm2.19  44137  jm2.26lem3  44145  kelac1  44202  mpaaeu  44289  radcnvrat  45435  binomcxplemnotnn0  45477  sqrtnegnre  48513  paireqne  48729  fmtnoprmfac1lem  48785  requad01  48855  requad2  48857  perfectALTVlem2  48956  nnsgrpnmnd  49411  isidom3  49578  rrx2pnedifcoorneor  49965  rrx2pnedifcoorneorr  49966  eenglngeehlnmlem2  49987  fdomne0  50097  oppcendc  50268  onetansqsecsq  51065