Theorem necon3bid 3004

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

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

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 2961

This theorem is used by:  neeq1d  3019  neeq2d  3020  neeq12d  3021  nebi  3040  pr1nebg  4825  f1dom3fv3dif  7271  frxp  8128  frxp2  8146  frxp3  8153  suppval1  8168  iinon  8333  fodomfib  9295  wemapso  9520  wemapso2lem  9521  infpssrlem4  10305  ttukeylem6  10513  fodomb  10525  tskcard  10783  addneintrd  11434  addneintr2d  11435  negne0bd  11579  negned  11583  subne0d  11595  subne0ad  11597  subneintrd  11630  subneintr2d  11632  divne0b  11900  div2neg  11955  divne1d  12019  div2sub  12057  xaddass2  13294  xadddi2  13341  seqf1olem1  14097  expne0  14149  sqne0  14179  hashneq0  14420  hashnncl  14422  hashgt0  14444  ccat1st1st  14688  pfxn0  14748  cjne0  15240  recval  15400  absgt0  15402  abs1m  15413  abslem2  15417  sqreulem  15437  sqreu  15438  absne0d  15527  geoserg  15945  geolim  15949  geolim2  15950  georeclim  15951  geoisum1c  15959  tanval2  16213  tanaddlem  16246  tanadd  16247  4sqlem11  17039  ipodrsima  18621  chnind  18701  chnub  18702  f1omvdmvd  19559  f1omvdcnv  19560  f1omvdconj  19562  pmtrfmvdn0  19578  sylow1lem4  19717  dprdf1o  20150  dprd2da  20160  ogrpsublt  20258  ringinvnz1ne0  20431  rrgsupp  20852  abvne0  20974  isfieldidl2  21439  gzrngunit  21635  chrnzr  21732  obsne0  21927  mdetdiaglem  22807  cnhaus  23563  hauscmplem  23615  fsubbas  24077  metn0  24570  nmne0  24829  nmgt0  24840  iccpnfhmeo  25157  ncvs1  25369  ipcau2  25446  dvcnvlem  26188  dvlip  26205  ftc1lem5  26252  mdegldg  26276  ply1divmo  26346  ig1peu  26385  ig1pdvds  26390  dgrmul  26480  coecj  26488  coecjOLD  26490  plydivlem4  26510  vieta1lem2  26525  vieta1  26526  aareccl  26542  geolim3  26555  abelthlem2  26648  abelthlem7  26654  tanregt0  26757  tanarg  26837  logtayl  26878  abscxp2  26911  cxpsqrt  26921  abscxpbnd  26971  logrec  26981  ang180lem1  27027  ang180lem2  27028  ang180lem3  27029  lawcos  27034  isosctr  27039  asinlem  27086  atandm2  27095  atandm4  27097  2efiatan  27136  tanatan  27137  atandmtan  27138  dvatan  27153  mersenne  27444  perfectlem2  27447  dchrinv  27478  dchrptlem2  27482  dchrsum2  27485  sumdchr2  27487  lgsabs1  27553  dchrisum0re  27730  ltsval2  27873  bday1  28060  cuteq1  28063  n0subs2  28610  tgcgrneq  28805  mirlni  29025  footexALT  29051  footexlem1  29052  footexlem2  29053  prlngsymquadlem  29270  colinearalg  29317  axsegconlem6  29329  axsegconlem9  29332  ax5seglem5  29340  axlowdimlem14  29362  wlkn0  30030  cyclnspth  30218  iswwlksnx  30258  wwlksm1edg  30299  wspthsnonn0vne  30335  umgrclwwlkge2  30411  clwwisshclwws  30435  hashecclwwlkn1  30497  umgrhashecclwwlk  30498  frgrregord013  30819  frgrogt3nreg  30821  friendshipgt3  30822  nrt2irr  30897  nvgt0  31099  nv1  31100  nmlnogt0  31222  nmblolbii  31224  blocnilem  31229  normne0  31555  normcan  32001  nmlnopne0  32424  nmophmi  32456  riesz3i  32487  hashne0  33226  wrdpmtrlast  33479  cycpmco2lem6  33517  1arithidom  33893  ply1unit  33931  m1pmeq  33941  minplyirredlem  34166  constrrtcclem  34190  constrconj  34201  iconstr  34222  zarclssn  34329  esumpcvgval  34534  ballotlemfrcn0  34987  signsply0  35005  signstfvn  35023  signsvtn0  35024  signstfvneq0  35026  signstfveq0a  35030  signshnz  35045  bnj168  35186  nummin  35544  usgrgt2cycl  35669  erdszelem9  35730  segcon2  36636  outsideofeu  36662  heicant  38365  smprngopr  38763  isfldidl2  38780  isdmn3  38785  lsat0cv  39867  lcvexchlem1  39868  lsatcvat2  39885  lkrshp  39939  lkrshp3  39940  lkrpssN  39997  cvrat2  40263  atcvrneN  40264  atcvrj2b  40266  2llnmat  40358  2lnat  40618  pmapjat1  40687  pclfinclN  40784  lautlt  40925  ltrn11at  40981  ltrnatneq  41016  trlcone  41562  tendoconid  41663  tendotr  41664  cdleml3N  41812  dochsordN  42208  dochn0nv  42209  djhcvat42  42249  dochsatshp  42285  lcfl8b  42338  lclkrlem2a  42341  lcfrlem9  42384  mapdsord  42489  mapdncol  42504  mapdpglem29  42534  mapdindp1  42554  hdmapnzcl  42679  hdmaprnlem1N  42683  hdmaprnlem3N  42684  hdmaprnlem3uN  42685  hdmaprnlem9N  42691  hdmap14lem9  42710  hgmapval1  42727  hgmapadd  42728  hgmapmul  42729  hgmaprnlem1N  42730  hdmaplkr  42747  hdmapip1  42750  hgmapvvlem1  42757  hgmapvvlem2  42758  hgmapvvlem3  42759  fldhmf1  42917  aks6d1c2p2  42946  aks6d1c5lem2  42965  aks6d1c6lem3  42999  redivne0bd  43271  fsuppind  43382  jm2.19  43780  jm2.26lem3  43788  kelac1  43850  mpaaeu  43937  radcnvrat  45084  binomcxplemnotnn0  45126  sqrtnegnre  48104  paireqne  48320  fmtnoprmfac1lem  48376  requad01  48446  requad2  48448  perfectALTVlem2  48547  nnsgrpnmnd  49002  isidom3  49169  rrx2pnedifcoorneor  49555  rrx2pnedifcoorneorr  49556  eenglngeehlnmlem2  49577  fdomne0  49687  oppcendc  49855  onetansqsecsq  50598