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 1570   ≠ 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  4818  f1dom3fv3dif  7266  frxp  8125  frxp2  8143  frxp3  8150  suppval1  8165  iinon  8330  fodomfib  9299  wemapso  9524  wemapso2lem  9525  infpssrlem4  10309  ttukeylem6  10517  fodomb  10530  tskcard  10791  addneintrd  11442  addneintr2d  11443  negne0bd  11587  negned  11591  subne0d  11604  subne0ad  11605  subneintrd  11638  subneintr2d  11640  divne0b  11908  div2neg  11963  divne1d  12027  div2sub  12065  xaddass2  13303  xadddi2  13350  seqf1olem1  14106  expne0  14158  sqne0  14188  hashneq0  14429  hashnncl  14431  hashgt0  14453  ccat1st1st  14697  pfxn0  14757  cjne0  15251  recval  15411  absgt0  15413  abs1m  15424  abslem2  15428  sqreulem  15448  sqreu  15449  absne0d  15538  geoserg  15956  geolim  15960  geolim2  15961  georeclim  15962  geoisum1c  15970  tanval2  16222  tanaddlem  16255  tanadd  16256  4sqlem11  17048  ipodrsima  18630  chnind  18710  chnub  18711  f1omvdmvd  19571  f1omvdcnv  19572  f1omvdconj  19574  pmtrfmvdn0  19590  sylow1lem4  19729  dprdf1o  20162  dprd2da  20172  ogrpsublt  20270  ringinvnz1ne0  20443  rrgsupp  20864  abvne0  20986  isfieldidl2  21451  gzrngunit  21647  chrnzr  21744  obsne0  21939  mdetdiaglem  22821  cnhaus  23580  hauscmplem  23632  fsubbas  24094  metn0  24587  nmne0  24846  nmgt0  24857  iccpnfhmeo  25174  ncvs1  25386  ipcau2  25463  dvcnvlem  26204  dvlip  26221  ftc1lem5  26268  mdegldg  26292  ply1divmo  26362  ig1peu  26401  ig1pdvds  26406  dgrmul  26497  coecj  26505  coecjOLD  26507  plydivlem4  26527  rnplynfin  26540  vieta1lem2  26544  vieta1  26545  aareccl  26563  geolim3  26576  abelthlem2  26669  abelthlem7  26675  tanregt0  26777  tanarg  26857  logtayl  26898  abscxp2  26931  cxpsqrt  26941  abscxpbnd  26991  logrec  27001  ang180lem1  27047  ang180lem2  27048  ang180lem3  27049  lawcos  27054  isosctr  27059  asinlem  27106  atandm2  27115  atandm4  27117  2efiatan  27156  tanatan  27157  atandmtan  27158  dvatan  27173  mersenne  27464  perfectlem2  27467  dchrinv  27498  dchrptlem2  27502  dchrsum2  27505  sumdchr2  27507  lgsabs1  27573  dchrisum0re  27750  ltsval2  27893  bday1  28080  cuteq1  28083  n0subs2  28630  tgcgrneq  28825  mirlni  29047  footexALT  29073  footexlem1  29074  footexlem2  29075  prlngsymquadlem  29321  colinearalg  29368  axsegconlem6  29380  axsegconlem9  29383  ax5seglem5  29391  axlowdimlem14  29413  wlkn0  30081  cyclnspth  30269  iswwlksnx  30309  wwlksm1edg  30350  wspthsnonn0vne  30386  umgrclwwlkge2  30462  clwwisshclwws  30486  hashecclwwlkn1  30548  umgrhashecclwwlk  30549  frgrregord013  30876  frgrogt3nreg  30878  friendshipgt3  30879  nrt2irr  30954  nvgt0  31156  nv1  31157  nmlnogt0  31279  nmblolbii  31281  blocnilem  31286  normne0  31612  normcan  32058  nmlnopne0  32481  nmophmi  32513  riesz3i  32544  hashne0  33281  wrdpmtrlast  33534  cycpmco2lem6  33572  1arithidom  33948  ply1unit  33986  m1pmeq  33996  minplyirredlem  34221  constrrtcclem  34245  constrconj  34256  iconstr  34277  zarclssn  34384  esumpcvgval  34589  ballotlemfrcn0  35042  signsply0  35060  signstfvn  35078  signsvtn0  35079  signstfvneq0  35081  signstfveq0a  35085  signshnz  35100  bnj168  35241  nummin  35599  usgrgt2cycl  35724  erdszelem9  35779  segcon2  36686  outsideofeu  36712  heicant  38405  smprngopr  38803  isfldidl2  38820  isdmn3  38825  lsat0cv  39907  lcvexchlem1  39908  lsatcvat2  39925  lkrshp  39979  lkrshp3  39980  lkrpssN  40037  cvrat2  40303  atcvrneN  40304  atcvrj2b  40306  2llnmat  40398  2lnat  40658  pmapjat1  40727  pclfinclN  40824  lautlt  40965  ltrn11at  41021  ltrnatneq  41056  trlcone  41602  tendoconid  41703  tendotr  41704  cdleml3N  41852  dochsordN  42248  dochn0nv  42249  djhcvat42  42289  dochsatshp  42325  lcfl8b  42378  lclkrlem2a  42381  lcfrlem9  42424  mapdsord  42529  mapdncol  42544  mapdpglem29  42574  mapdindp1  42594  hdmapnzcl  42719  hdmaprnlem1N  42723  hdmaprnlem3N  42724  hdmaprnlem3uN  42725  hdmaprnlem9N  42731  hdmap14lem9  42750  hgmapval1  42767  hgmapadd  42768  hgmapmul  42769  hgmaprnlem1N  42770  hdmaplkr  42787  hdmapip1  42790  hgmapvvlem1  42797  hgmapvvlem2  42798  hgmapvvlem3  42799  fldhmf1  42957  aks6d1c2p2  42986  aks6d1c5lem2  43005  aks6d1c6lem3  43039  redivne0bd  43326  fsuppind  43437  jm2.19  43835  jm2.26lem3  43843  kelac1  43905  mpaaeu  43992  radcnvrat  45139  binomcxplemnotnn0  45181  sqrtnegnre  48196  paireqne  48412  fmtnoprmfac1lem  48468  requad01  48538  requad2  48540  perfectALTVlem2  48639  nnsgrpnmnd  49094  isidom3  49261  rrx2pnedifcoorneor  49647  rrx2pnedifcoorneorr  49648  eenglngeehlnmlem2  49669  fdomne0  49779  oppcendc  49945  onetansqsecsq  50688