Theorem necon3bid 2985

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  neeq1d  3000  neeq2d  3001  neeq12d  3002  nebi  3021  pr1nebg  4858  f1dom3fv3dif  7288  frxp  8151  frxp2  8169  frxp3  8176  suppval1  8191  iinon  8380  fodomfib  9369  fodomfibOLD  9371  wemapso  9591  wemapso2lem  9592  infpssrlem4  10346  ttukeylem6  10554  fodomb  10566  tskcard  10821  addneintrd  11468  addneintr2d  11469  negne0bd  11613  negned  11617  subne0d  11629  subne0ad  11631  subneintrd  11664  subneintr2d  11666  divne0b  11933  div2neg  11990  divne1d  12054  div2sub  12092  xaddass2  13292  xadddi2  13339  seqf1olem1  14082  expne0  14134  sqne0  14163  hashneq0  14403  hashnncl  14405  hashgt0  14427  ccat1st1st  14666  pfxn0  14724  cjne0  15202  recval  15361  absgt0  15363  abs1m  15374  abslem2  15378  sqreulem  15398  sqreu  15399  absne0d  15486  geoserg  15902  geolim  15906  geolim2  15907  georeclim  15908  geoisum1c  15916  tanval2  16169  tanaddlem  16202  tanadd  16203  4sqlem11  16993  ipodrsima  18586  f1omvdmvd  19461  f1omvdcnv  19462  f1omvdconj  19464  pmtrfmvdn0  19480  sylow1lem4  19619  dprdf1o  20052  dprd2da  20062  ringinvnz1ne0  20297  rrgsupp  20701  abvne0  20820  gzrngunit  21451  chrnzr  21545  obsne0  21745  mdetdiaglem  22604  cnhaus  23362  hauscmplem  23414  fsubbas  23875  metn0  24370  nmne0  24632  nmgt0  24643  iccpnfhmeo  24976  ncvs1  25191  ipcau2  25268  dvcnvlem  26014  dvlip  26032  ftc1lem5  26081  mdegldg  26105  ply1divmo  26175  ig1peu  26214  ig1pdvds  26219  dgrmul  26310  coecj  26318  coecjOLD  26320  plydivlem4  26338  vieta1lem2  26353  vieta1  26354  aareccl  26368  geolim3  26381  abelthlem2  26476  abelthlem7  26482  tanregt0  26581  tanarg  26661  logtayl  26702  abscxp2  26735  cxpsqrt  26745  abscxpbnd  26796  logrec  26806  ang180lem1  26852  ang180lem2  26853  ang180lem3  26854  lawcos  26859  isosctr  26864  asinlem  26911  atandm2  26920  atandm4  26922  2efiatan  26961  tanatan  26962  atandmtan  26963  dvatan  26978  mersenne  27271  perfectlem2  27274  dchrinv  27305  dchrptlem2  27309  dchrsum2  27312  sumdchr2  27314  lgsabs1  27380  dchrisum0re  27557  sltval2  27701  bday1s  27876  cuteq1  27878  tgcgrneq  28491  footexALT  28726  footexlem1  28727  footexlem2  28728  colinearalg  28925  axsegconlem6  28937  axsegconlem9  28940  ax5seglem5  28948  axlowdimlem14  28970  wlkn0  29639  cyclnspth  29821  iswwlksnx  29860  wwlksm1edg  29901  wspthsnonn0vne  29937  umgrclwwlkge2  30010  clwwisshclwws  30034  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  frgrregord013  30414  frgrogt3nreg  30416  friendshipgt3  30417  nrt2irr  30492  nvgt0  30693  nv1  30694  nmlnogt0  30816  nmblolbii  30818  blocnilem  30823  normne0  31149  normcan  31595  nmlnopne0  32018  nmophmi  32050  riesz3i  32081  chnind  33001  chnub  33002  ogrpsublt  33098  wrdpmtrlast  33113  cycpmco2lem6  33151  1arithidom  33565  ply1unit  33600  m1pmeq  33608  minplyirredlem  33753  constrrtcclem  33775  constrconj  33786  zarclssn  33872  esumpcvgval  34079  ballotlemfrcn0  34532  signsply0  34566  signstfvn  34584  signsvtn0  34585  signstfvneq0  34587  signstfveq0a  34591  signshnz  34606  bnj168  34744  nummin  35105  usgrgt2cycl  35135  erdszelem9  35204  segcon2  36106  outsideofeu  36132  heicant  37662  smprngopr  38059  isfldidl2  38076  isdmn3  38081  lsat0cv  39034  lcvexchlem1  39035  lsatcvat2  39052  lkrshp  39106  lkrshp3  39107  lkrpssN  39164  cvrat2  39431  atcvrneN  39432  atcvrj2b  39434  2llnmat  39526  2lnat  39786  pmapjat1  39855  pclfinclN  39952  lautlt  40093  ltrn11at  40149  ltrnatneq  40184  trlcone  40730  tendoconid  40831  tendotr  40832  cdleml3N  40980  dochsordN  41376  dochn0nv  41377  djhcvat42  41417  dochsatshp  41453  lcfl8b  41506  lclkrlem2a  41509  lcfrlem9  41552  mapdsord  41657  mapdncol  41672  mapdpglem29  41702  mapdindp1  41722  hdmapnzcl  41847  hdmaprnlem1N  41851  hdmaprnlem3N  41852  hdmaprnlem3uN  41853  hdmaprnlem9N  41859  hdmap14lem9  41878  hgmapval1  41895  hgmapadd  41896  hgmapmul  41897  hgmaprnlem1N  41898  hdmaplkr  41915  hdmapip1  41918  hgmapvvlem1  41925  hgmapvvlem2  41926  hgmapvvlem3  41927  fldhmf1  42091  aks6d1c2p2  42120  aks6d1c5lem2  42139  aks6d1c6lem3  42173  fsuppind  42600  jm2.19  43005  jm2.26lem3  43013  kelac1  43075  mpaaeu  43162  radcnvrat  44333  binomcxplemnotnn0  44375  sqrtnegnre  47319  paireqne  47498  fmtnoprmfac1lem  47551  requad01  47608  requad2  47610  perfectALTVlem2  47709  nnsgrpnmnd  48094  rrx2pnedifcoorneor  48637  rrx2pnedifcoorneorr  48638  eenglngeehlnmlem2  48659  fdomne0  48759  oppcendc  48906  onetansqsecsq  49280