Theorem necon3bid 2978

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  neeq1d  2993  neeq2d  2994  neeq12d  2995  nebi  3014  pr1nebg  4789  f1dom3fv3dif  7212  frxp  8066  frxp2  8084  frxp3  8091  suppval1  8106  iinon  8270  fodomfib  9229  fodomfibOLD  9231  wemapso  9456  wemapso2lem  9457  infpssrlem4  10219  ttukeylem6  10427  fodomb  10439  tskcard  10695  addneintrd  11344  addneintr2d  11345  negne0bd  11489  negned  11493  subne0d  11505  subne0ad  11507  subneintrd  11540  subneintr2d  11542  divne0b  11811  div2neg  11869  divne1d  11933  div2sub  11971  xaddass2  13193  xadddi2  13240  seqf1olem1  13994  expne0  14046  sqne0  14076  hashneq0  14317  hashnncl  14319  hashgt0  14341  ccat1st1st  14582  pfxn0  14640  cjne0  15116  recval  15276  absgt0  15278  abs1m  15289  abslem2  15293  sqreulem  15313  sqreu  15314  absne0d  15403  geoserg  15822  geolim  15826  geolim2  15827  georeclim  15828  geoisum1c  15836  tanval2  16091  tanaddlem  16124  tanadd  16125  4sqlem11  16917  ipodrsima  18498  chnind  18578  chnub  18579  f1omvdmvd  19409  f1omvdcnv  19410  f1omvdconj  19412  pmtrfmvdn0  19428  sylow1lem4  19567  dprdf1o  20000  dprd2da  20010  ogrpsublt  20108  ringinvnz1ne0  20272  rrgsupp  20673  abvne0  20791  gzrngunit  21408  chrnzr  21505  obsne0  21700  mdetdiaglem  22581  cnhaus  23337  hauscmplem  23389  fsubbas  23850  metn0  24343  nmne0  24602  nmgt0  24613  iccpnfhmeo  24930  ncvs1  25142  ipcau2  25219  dvcnvlem  25961  dvlip  25978  ftc1lem5  26025  mdegldg  26049  ply1divmo  26119  ig1peu  26158  ig1pdvds  26163  dgrmul  26253  coecj  26261  coecjOLD  26263  plydivlem4  26280  vieta1lem2  26295  vieta1  26296  aareccl  26310  geolim3  26323  abelthlem2  26415  abelthlem7  26421  tanregt0  26521  tanarg  26601  logtayl  26642  abscxp2  26675  cxpsqrt  26685  abscxpbnd  26735  logrec  26745  ang180lem1  26791  ang180lem2  26792  ang180lem3  26793  lawcos  26798  isosctr  26803  asinlem  26850  atandm2  26859  atandm4  26861  2efiatan  26900  tanatan  26901  atandmtan  26902  dvatan  26917  mersenne  27208  perfectlem2  27211  dchrinv  27242  dchrptlem2  27246  dchrsum2  27249  sumdchr2  27251  lgsabs1  27317  dchrisum0re  27494  ltsval2  27638  bday1  27824  cuteq1  27827  n0subs2  28374  tgcgrneq  28569  footexALT  28804  footexlem1  28805  footexlem2  28806  colinearalg  28997  axsegconlem6  29009  axsegconlem9  29012  ax5seglem5  29020  axlowdimlem14  29042  wlkn0  29707  cyclnspth  29887  iswwlksnx  29926  wwlksm1edg  29967  wspthsnonn0vne  30003  umgrclwwlkge2  30079  clwwisshclwws  30103  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  frgrregord013  30483  frgrogt3nreg  30485  friendshipgt3  30486  nrt2irr  30561  nvgt0  30763  nv1  30764  nmlnogt0  30886  nmblolbii  30888  blocnilem  30893  normne0  31219  normcan  31665  nmlnopne0  32088  nmophmi  32120  riesz3i  32151  hashne0  32902  wrdpmtrlast  33174  cycpmco2lem6  33212  1arithidom  33620  ply1unit  33658  m1pmeq  33668  minplyirredlem  33894  constrrtcclem  33918  constrconj  33929  iconstr  33950  zarclssn  34057  esumpcvgval  34262  ballotlemfrcn0  34714  signsply0  34735  signstfvn  34753  signsvtn0  34754  signstfvneq0  34756  signstfveq0a  34760  signshnz  34775  bnj168  34913  nummin  35274  usgrgt2cycl  35358  erdszelem9  35427  segcon2  36333  outsideofeu  36359  heicant  38022  smprngopr  38419  isfldidl2  38436  isdmn3  38441  lsat0cv  39525  lcvexchlem1  39526  lsatcvat2  39543  lkrshp  39597  lkrshp3  39598  lkrpssN  39655  cvrat2  39921  atcvrneN  39922  atcvrj2b  39924  2llnmat  40016  2lnat  40276  pmapjat1  40345  pclfinclN  40442  lautlt  40583  ltrn11at  40639  ltrnatneq  40674  trlcone  41220  tendoconid  41321  tendotr  41322  cdleml3N  41470  dochsordN  41866  dochn0nv  41867  djhcvat42  41907  dochsatshp  41943  lcfl8b  41996  lclkrlem2a  41999  lcfrlem9  42042  mapdsord  42147  mapdncol  42162  mapdpglem29  42192  mapdindp1  42212  hdmapnzcl  42337  hdmaprnlem1N  42341  hdmaprnlem3N  42342  hdmaprnlem3uN  42343  hdmaprnlem9N  42349  hdmap14lem9  42368  hgmapval1  42385  hgmapadd  42386  hgmapmul  42387  hgmaprnlem1N  42388  hdmaplkr  42405  hdmapip1  42408  hgmapvvlem1  42415  hgmapvvlem2  42416  hgmapvvlem3  42417  fldhmf1  42575  aks6d1c2p2  42604  aks6d1c5lem2  42623  aks6d1c6lem3  42657  redivne0bd  42927  fsuppind  43040  jm2.19  43438  jm2.26lem3  43446  kelac1  43508  mpaaeu  43595  radcnvrat  44758  binomcxplemnotnn0  44800  sqrtnegnre  47770  paireqne  47986  fmtnoprmfac1lem  48042  requad01  48112  requad2  48114  perfectALTVlem2  48213  nnsgrpnmnd  48669  rrx2pnedifcoorneor  49207  rrx2pnedifcoorneorr  49208  eenglngeehlnmlem2  49229  fdomne0  49340  oppcendc  49508  onetansqsecsq  50251