Theorem necon3bid 2969

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

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

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 2926

This theorem is referenced by:  neeq1d  2984  neeq2d  2985  neeq12d  2986  nebi  3005  pr1nebg  4822  f1dom3fv3dif  7243  frxp  8105  frxp2  8123  frxp3  8130  suppval1  8145  iinon  8309  fodomfib  9280  fodomfibOLD  9282  wemapso  9504  wemapso2lem  9505  infpssrlem4  10259  ttukeylem6  10467  fodomb  10479  tskcard  10734  addneintrd  11381  addneintr2d  11382  negne0bd  11526  negned  11530  subne0d  11542  subne0ad  11544  subneintrd  11577  subneintr2d  11579  divne0b  11848  div2neg  11905  divne1d  11969  div2sub  12007  xaddass2  13210  xadddi2  13257  seqf1olem1  14006  expne0  14058  sqne0  14088  hashneq0  14329  hashnncl  14331  hashgt0  14353  ccat1st1st  14593  pfxn0  14651  cjne0  15129  recval  15289  absgt0  15291  abs1m  15302  abslem2  15306  sqreulem  15326  sqreu  15327  absne0d  15416  geoserg  15832  geolim  15836  geolim2  15837  georeclim  15838  geoisum1c  15846  tanval2  16101  tanaddlem  16134  tanadd  16135  4sqlem11  16926  ipodrsima  18500  f1omvdmvd  19373  f1omvdcnv  19374  f1omvdconj  19376  pmtrfmvdn0  19392  sylow1lem4  19531  dprdf1o  19964  dprd2da  19974  ringinvnz1ne0  20209  rrgsupp  20610  abvne0  20728  gzrngunit  21350  chrnzr  21440  obsne0  21634  mdetdiaglem  22485  cnhaus  23241  hauscmplem  23293  fsubbas  23754  metn0  24248  nmne0  24507  nmgt0  24518  iccpnfhmeo  24843  ncvs1  25057  ipcau2  25134  dvcnvlem  25880  dvlip  25898  ftc1lem5  25947  mdegldg  25971  ply1divmo  26041  ig1peu  26080  ig1pdvds  26085  dgrmul  26176  coecj  26184  coecjOLD  26186  plydivlem4  26204  vieta1lem2  26219  vieta1  26220  aareccl  26234  geolim3  26247  abelthlem2  26342  abelthlem7  26348  tanregt0  26448  tanarg  26528  logtayl  26569  abscxp2  26602  cxpsqrt  26612  abscxpbnd  26663  logrec  26673  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  lawcos  26726  isosctr  26731  asinlem  26778  atandm2  26787  atandm4  26789  2efiatan  26828  tanatan  26829  atandmtan  26830  dvatan  26845  mersenne  27138  perfectlem2  27141  dchrinv  27172  dchrptlem2  27176  dchrsum2  27179  sumdchr2  27181  lgsabs1  27247  dchrisum0re  27424  sltval2  27568  bday1s  27743  cuteq1  27746  n0subs2  28254  tgcgrneq  28410  footexALT  28645  footexlem1  28646  footexlem2  28647  colinearalg  28837  axsegconlem6  28849  axsegconlem9  28852  ax5seglem5  28860  axlowdimlem14  28882  wlkn0  29549  cyclnspth  29731  iswwlksnx  29770  wwlksm1edg  29811  wspthsnonn0vne  29847  umgrclwwlkge2  29920  clwwisshclwws  29944  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  frgrregord013  30324  frgrogt3nreg  30326  friendshipgt3  30327  nrt2irr  30402  nvgt0  30603  nv1  30604  nmlnogt0  30726  nmblolbii  30728  blocnilem  30733  normne0  31059  normcan  31505  nmlnopne0  31928  nmophmi  31960  riesz3i  31991  hashne0  32735  chnind  32937  chnub  32938  ogrpsublt  33035  wrdpmtrlast  33050  cycpmco2lem6  33088  1arithidom  33508  ply1unit  33544  m1pmeq  33552  minplyirredlem  33700  constrrtcclem  33724  constrconj  33735  iconstr  33756  zarclssn  33863  esumpcvgval  34068  ballotlemfrcn0  34521  signsply0  34542  signstfvn  34560  signsvtn0  34561  signstfvneq0  34563  signstfveq0a  34567  signshnz  34582  bnj168  34720  nummin  35081  usgrgt2cycl  35117  erdszelem9  35186  segcon2  36093  outsideofeu  36119  heicant  37649  smprngopr  38046  isfldidl2  38063  isdmn3  38068  lsat0cv  39026  lcvexchlem1  39027  lsatcvat2  39044  lkrshp  39098  lkrshp3  39099  lkrpssN  39156  cvrat2  39423  atcvrneN  39424  atcvrj2b  39426  2llnmat  39518  2lnat  39778  pmapjat1  39847  pclfinclN  39944  lautlt  40085  ltrn11at  40141  ltrnatneq  40176  trlcone  40722  tendoconid  40823  tendotr  40824  cdleml3N  40972  dochsordN  41368  dochn0nv  41369  djhcvat42  41409  dochsatshp  41445  lcfl8b  41498  lclkrlem2a  41501  lcfrlem9  41544  mapdsord  41649  mapdncol  41664  mapdpglem29  41694  mapdindp1  41714  hdmapnzcl  41839  hdmaprnlem1N  41843  hdmaprnlem3N  41844  hdmaprnlem3uN  41845  hdmaprnlem9N  41851  hdmap14lem9  41870  hgmapval1  41887  hgmapadd  41888  hgmapmul  41889  hgmaprnlem1N  41890  hdmaplkr  41907  hdmapip1  41910  hgmapvvlem1  41917  hgmapvvlem2  41918  hgmapvvlem3  41919  fldhmf1  42078  aks6d1c2p2  42107  aks6d1c5lem2  42126  aks6d1c6lem3  42160  fsuppind  42578  jm2.19  42982  jm2.26lem3  42990  kelac1  43052  mpaaeu  43139  radcnvrat  44303  binomcxplemnotnn0  44345  sqrtnegnre  47308  paireqne  47512  fmtnoprmfac1lem  47565  requad01  47622  requad2  47624  perfectALTVlem2  47723  nnsgrpnmnd  48166  rrx2pnedifcoorneor  48705  rrx2pnedifcoorneorr  48706  eenglngeehlnmlem2  48727  fdomne0  48838  oppcendc  49007  onetansqsecsq  49750