Theorem eqnetrd 3023

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqnetrd.2	⊢ (𝜑 → 𝐵 ≠ 𝐶)

Assertion

Ref	Expression
eqnetrd	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem eqnetrd

Step	Hyp	Ref	Expression
1		eqnetrd.2	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
2		eqnetrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	neeq1d 3015	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
4	1, 3	mpbird 260	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  eqnetrrd  3024  3netr4d  3033  opnz  5442  xpdifid  6159  undefne0  8290  onoviun  8344  intrnfi  9401  cantnfp1lem2  9673  cantnfp1lem3  9674  wemapwe  9691  acndom2  10126  fin23lem14  10404  fin23lem40  10422  isf32lem6  10429  isf34lem5  10449  isf34lem7  10450  isf34lem6  10451  axcc2lem  10507  xaddnemnf  13359  xaddnepnf  13360  fseqsupcl  14113  hashprg  14532  elprchashprn2  14533  hash1n0  14559  limsupgre  15641  isercolllem3  15827  prodfn0  16056  ntrivcvgtail  16062  fproddiv  16121  fprodn0  16139  tanval3  16295  tanneg  16309  ruclem11  16401  nn0rppwr  16728  bezoutr1  16737  phibndlem  16940  dfphi2  16944  0ram  17191  0ram2  17192  ram0  17193  0ramcl  17194  gsumval2  18868  sgrp2nmndlem5  19121  issubg2  19345  ghmrn  19436  pmtrmvd  19663  gsumval3  20114  pgpfaclem2  20291  ablfaclem2  20295  ablfaclem3  20296  fincygsubgodd  20321  subdrgint  21053  abvdom  21080  lbsextlem2  21430  qsidomlem2  21630  cndrng  21700  gzrngunit  21732  zringunit  21765  cnmsgnsubg  21876  frlmssuvc2  22094  mhpmulcl  22463  iinopn  23213  cnconn  23733  1stcfb  23756  dissnlocfin  23841  fbasrn  24196  fclscmpi  24341  alexsublem  24356  ustuqtop5  24557  cnextucn  24614  dscmet  24884  reperflem  25131  evth  25273  cmetcaulem  25602  iscmet3  25607  metsscmetcld  25629  cmetss  25630  bcthlem5  25642  bcth2  25644  mbflimsup  25980  itg1addlem4  26013  itg1climres  26028  itg2monolem1  26064  itg2i1fseq2  26070  tdeglem4  26371  deg1add  26414  deg1mul2  26425  deg1tm  26430  dgreq  26556  dgradd2  26580  dgrmul  26582  dgrmulc  26583  dgrcolem1  26585  plyrem  26619  facth  26620  fta1lem  26621  vieta1lem1  26626  vieta1lem2  26627  vieta1  26628  qaa  26640  aareccl  26646  geolim3  26659  aaliou3lem9  26670  coseq00topi  26824  cosne0  26850  tanord  26859  tanarg  26940  cxpne0  26998  cxpsqrt  27024  logbrec  27103  chordthmlem  27153  chordthmlem2  27154  dcubic  27167  mcubic  27168  cubic2  27169  cubic  27170  quartlem4  27181  atandmneg  27227  atandmcj  27230  atancj  27231  atanrecl  27232  atanlogsublem  27236  efiatan2  27238  tanatan  27240  atandmtan  27241  cosatan  27242  cosatanne0  27243  wilthlem2  27389  ftalem7  27399  basellem2  27402  basellem4  27404  basellem5  27405  isppw  27434  dchrptlem2  27585  lgsne0  27655  2sqlem8a  27745  2sqlem8  27746  noseponlem  28014  recsne0  28571  tglnpt2  29114  midexlem  29157  colperpexlem3  29201  mideulem2  29203  lnopp2hpgb  29234  angmgmaddov1  29381  subgruhgredgd  29858  wwlksnext  30475  wspthsnonn0vne  30499  clwwisshclwws  30599  vdn0conngrumgrv2  30790  vdgn1frgrv2  30890  nrt2irr  31067  ifnetrue  33136  ifnefals  33137  imadifxp  33188  acunirnmpt  33246  fnpreimac  33257  quad3d  33334  xaddeq0  33338  pmtrcnelor  33645  domnprodn0  33832  domnprodeq0  33833  drnglring  34017  dflringlem3  34021  dflring4  34023  ply1dg3rt0irred  34109  m1pmeq  34110  mplmulmvr  34164  esplyfvaln  34199  esplyind  34200  ply1annnr  34328  minplyirred  34336  rtelextdg2lem  34351  constrrtcclem  34359  constrconj  34370  constrext2chnlem  34375  constrremulcl  34392  constrrecl  34394  constrreinvcl  34397  2sqr3minply  34405  2sqr3nconstr  34406  cos9thpiminplylem1  34407  cos9thpiminplylem2  34408  cos9thpiminplylem3  34409  cos9thpiminply  34413  cos9thpinconstrlem1  34414  cos9thpinconstrlem2  34415  cos9thpinconstr  34416  madjusmdetlem2  34453  zar0ring  34503  xrge0iifhom  34562  signswn0  35182  signsvtn0  35192  signstfvneq0  35194  repr0  35233  kard0b  35810  derangenlem  35915  subfacp1lem3  35926  subfacp1lem5  35928  wsuclem  36567  ivthALT  37103  neibastop1  37127  weiunfrlem  37232  mh-inf3f1  37309  finxpreclem2  38293  finxpreclem6  38299  tan2h  38515  poimirlem9  38527  heicant  38553  itg2addnclem2  38570  lsatfixedN  40046  islshpat  40054  lkrshp  40142  2llnm3N  40606  dalemdnee  40703  cdleme18b  41329  cdleme40m  41504  cdlemg12g  41686  cdlemh  41854  cdlemj3  41860  tendoconid  41866  cdlemk3  41870  cdlemk12  41887  cdlemk12u  41909  cdlemk46  41985  cdlemk54  41995  erngdvlem4  42028  erngdvlem4-rN  42036  dibn0  42190  dihglblem2aN  42330  dochshpncl  42421  dochsnnz  42487  dochsatshpb  42489  lcfl7lem  42536  lcfl8b  42541  lcfrlem33  42612  lcfr  42622  hdmaprnlem3uN  42888  aks4d1p1p7  43104  fldhmf1  43120  primrootspoweq0  43136  idomnnzpownz  43162  idomnnzgmulnz  43163  aks6d1c5lem2  43168  deg1gprod  43170  unitscyglem4  43228  25or6to4  43236  tanhalfpim  43380  remul01  43438  remulinvcom  43464  domnexpgn0cl  43564  ricdrng1  43572  prjcrv0  43649  3cubeslem2  43675  cmpfiiin  43687  pell1234qrne0  43839  rmxyneg  43906  fnwe2lem2  44037  kelac1  44049  wnefimgd  45146  radcnvrat  45283  binomcxplemfrat  45320  binomcxplemradcnv  45321  disjrnmpt2  46172  disjf1o  46175  choicefi  46183  ioondisj2  46474  ioondisj1  46475  lptioo2  46612  lptioo1  46613  0ellimcdiv  46628  liminflbuz2  46794  ioodvbdlimc1  46912  ioodvbdlimc2  46914  stoweidlem31  47010  stoweidlem59  47038  wallispilem4  47047  wallispi  47049  stirlinglem3  47055  stirlinglem14  47066  dirkerper  47075  dirkertrigeq  47080  dirkercncflem2  47083  fourierdlem4  47090  fourierdlem30  47116  fourierdlem41  47127  fourierdlem42  47128  fourierdlem44  47130  fourierdlem46  47131  fourierdlem48  47133  fourierdlem49  47134  fourierdlem62  47147  fourierdlem74  47159  fourierdlem75  47160  fourierdlem79  47164  fourierdlem102  47187  fourierdlem114  47199  fouriersw  47210  elaa2lem  47212  elaa2  47213  etransclem24  47237  etransclem44  47257  etransclem47  47260  ioorrnopnlem  47283  subsaliuncl  47337  sge0cl  47360  meadjun  47441  meadjiunlem  47444  hoicvr  47527  ovnsubadd2lem  47624  smflimlem6  47755  smfpimcc  47787  smflimsuplem2  47800  sqrtnnaa  47882  sqrtnzqaa  47883  cjnpoly  47908  modm2nep1  48411  modm1nep2  48413  modm1p1ne  48415  lswn0  48495  sprvalpwn0  48534  fmtnoprmfac1lem  48618  grimuhgr  48954  gpg3nbgrvtx0  49143  el0ldep  49547  islindeps2  49564  ldepsnlinclem1  49586  ldepsnlinclem2  49587  itscnhlinecirc02plem1  49863  ovconstbrd  49941  ovconstbrn0d  49942  catprs  50088  fucofvalne  50402  crosspv2d  50930  crosspv3d  50931