Theorem eqnetrd 3026

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 3018	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
4	1, 3	mpbird 260	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqnetrrd  3027  3netr4d  3036  opnz  5449  xpdifid  6177  undefne0  8335  onoviun  8389  intrnfi  9445  cantnfp1lem2  9717  cantnfp1lem3  9718  wemapwe  9735  acndom2  10172  fin23lem14  10450  fin23lem40  10468  isf32lem6  10475  isf34lem5  10495  isf34lem7  10496  isf34lem6  10497  axcc2lem  10553  xaddnemnf  13406  xaddnepnf  13407  fseqsupcl  14160  hashprg  14580  elprchashprn2  14581  hash1n0  14607  limsupgre  15692  isercolllem3  15878  prodfn0  16107  ntrivcvgtail  16113  fproddiv  16172  fprodn0  16190  tanval3  16346  tanneg  16360  ruclem11  16452  nn0rppwr  16779  bezoutr1  16788  phibndlem  16991  dfphi2  16995  0ram  17242  0ram2  17243  ram0  17244  0ramcl  17245  gsumval2  18925  sgrp2nmndlem5  19178  issubg2  19402  ghmrn  19493  pmtrmvd  19721  gsumval3  20172  pgpfaclem2  20349  ablfaclem2  20353  ablfaclem3  20354  fincygsubgodd  20379  subdrgint  21111  abvdom  21138  lbsextlem2  21488  qsidomlem2  21688  cndrng  21759  gzrngunit  21793  zringunit  21827  cnmsgnsubg  21938  frlmssuvc2  22156  mhpmulcl  22525  iinopn  23275  cnconn  23795  1stcfb  23818  dissnlocfin  23903  fbasrn  24258  fclscmpi  24403  alexsublem  24418  ustuqtop5  24619  cnextucn  24676  dscmet  24946  reperflem  25193  evth  25335  cmetcaulem  25664  iscmet3  25669  metsscmetcld  25691  cmetss  25692  bcthlem5  25704  bcth2  25706  mbflimsup  26042  itg1addlem4  26075  itg1climres  26090  itg2monolem1  26126  itg2i1fseq2  26132  tdeglem4  26433  deg1add  26476  deg1mul2  26487  deg1tm  26492  dgreq  26618  dgradd2  26642  dgrmul  26644  dgrmulc  26645  dgrcolem1  26647  plyrem  26681  facth  26682  fta1lem  26683  vieta1lem1  26688  vieta1lem2  26689  vieta1  26690  qaa  26704  aareccl  26710  geolim3  26723  aaliou3lem9  26734  coseq00topi  26888  cosne0  26914  tanord  26923  tanarg  27004  cxpne0  27062  cxpsqrt  27088  logbrec  27167  chordthmlem  27217  chordthmlem2  27218  dcubic  27231  mcubic  27232  cubic2  27233  cubic  27234  quartlem4  27245  atandmneg  27291  atandmcj  27294  atancj  27295  atanrecl  27296  atanlogsublem  27300  efiatan2  27302  tanatan  27304  atandmtan  27305  cosatan  27306  cosatanne0  27307  wilthlem2  27453  ftalem7  27463  basellem2  27466  basellem4  27468  basellem5  27469  isppw  27498  dchrptlem2  27649  lgsne0  27719  2sqlem8a  27809  2sqlem8  27810  noseponlem  28078  recsne0  28635  tglnpt2  29178  midexlem  29221  colperpexlem3  29265  mideulem2  29267  lnopp2hpgb  29298  angmgmaddov1  29445  subgruhgredgd  29922  wwlksnext  30539  wspthsnonn0vne  30563  clwwisshclwws  30663  vdn0conngrumgrv2  30854  vdgn1frgrv2  30954  nrt2irr  31131  tgextamirnhl  33129  ifnetrue  33241  ifnefals  33242  imadifxp  33293  acunirnmpt  33351  fnpreimac  33362  quad3d  33437  xaddeq0  33441  pmtrcnelor  33751  domnprodn0  33938  domnprodeq0  33939  drnglring  34128  dflringlem3  34132  dflring4  34134  ply1dg3rt0irred  34219  m1pmeq  34220  rngunsnply1chr2lem2  34251  mplmulmvr  34282  esplyfvaln  34317  esplyind  34318  ply1annnr  34446  minplyirred  34454  rtelextdg2lem  34469  constrrtcclem  34477  constrconj  34488  constrext2chnlem  34493  constrremulcl  34510  constrrecl  34512  constrreinvcl  34515  2sqr3minply  34523  2sqr3nconstr  34524  cos9thpiminplylem1  34525  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminply  34531  cos9thpinconstrlem1  34532  cos9thpinconstrlem2  34533  cos9thpinconstr  34534  madjusmdetlem2  34571  zar0ring  34621  xrge0iifhom  34680  signswn0  35300  signsvtn0  35310  signstfvneq0  35312  repr0  35351  kard0b  35968  fnlfvk3n0  36069  derangenlem  36144  subfacp1lem3  36155  subfacp1lem5  36157  wsuclem  36802  ivthALT  37338  neibastop1  37362  weiunfrlem  37467  mh-inf3f1  37544  finxpreclem2  38581  finxpreclem6  38587  tan2h  38803  poimirlem9  38815  heicant  38841  itg2addnclem2  38858  lsatfixedN  40332  islshpat  40340  lkrshp  40428  2llnm3N  40892  dalemdnee  40989  cdleme18b  41615  cdleme40m  41790  cdlemg12g  41972  cdlemh  42140  cdlemj3  42146  tendoconid  42152  cdlemk3  42156  cdlemk12  42173  cdlemk12u  42195  cdlemk46  42271  cdlemk54  42281  erngdvlem4  42314  erngdvlem4-rN  42322  dibn0  42476  dihglblem2aN  42616  dochshpncl  42707  dochsnnz  42773  dochsatshpb  42775  lcfl7lem  42822  lcfl8b  42827  lcfrlem33  42898  lcfr  42908  hdmaprnlem3uN  43174  aks4d1p1p7  43390  fldhmf1  43406  primrootspoweq0  43422  idomnnzpownz  43448  idomnnzgmulnz  43449  aks6d1c5lem2  43454  deg1gprod  43456  unitscyglem4  43514  25or6to4  43522  tanhalfpim  43666  remul01  43724  remulinvcom  43750  domnexpgn0cl  43850  ricdrng1  43858  prjcrv0  43935  3cubeslem2  43961  cmpfiiin  43974  pell1234qrne0  44126  rmxyneg  44193  kelac1  44331  wnefimgd  45422  radcnvrat  45559  binomcxplemfrat  45596  binomcxplemradcnv  45597  disjrnmpt2  46476  disjf1o  46479  choicefi  46487  ioondisj2  46778  ioondisj1  46779  lptioo2  46916  lptioo1  46917  0ellimcdiv  46932  liminflbuz2  47098  ioodvbdlimc1  47216  ioodvbdlimc2  47218  stoweidlem31  47314  stoweidlem59  47342  wallispilem4  47351  wallispi  47353  stirlinglem3  47359  stirlinglem14  47370  dirkerper  47379  dirkertrigeq  47384  dirkercncflem2  47387  fourierdlem4  47394  fourierdlem30  47420  fourierdlem41  47431  fourierdlem42  47432  fourierdlem44  47434  fourierdlem46  47435  fourierdlem48  47437  fourierdlem49  47438  fourierdlem62  47451  fourierdlem74  47463  fourierdlem75  47464  fourierdlem79  47468  fourierdlem102  47491  fourierdlem114  47503  fouriersw  47514  elaa2lem  47516  elaa2  47517  etransclem24  47541  etransclem44  47561  etransclem47  47564  ioorrnopnlem  47587  subsaliuncl  47641  sge0cl  47664  meadjun  47745  meadjiunlem  47748  hoicvr  47831  ovnsubadd2lem  47928  smflimlem6  48059  smfpimcc  48091  smflimsuplem2  48104  sqrtnnaa  48186  sqrtnzqaa  48187  cjnpoly  48212  modm2nep1  48715  modm1nep2  48717  modm1p1ne  48719  lswn0  48799  sprvalpwn0  48838  fmtnoprmfac1lem  48922  grimuhgr  49258  gpg3nbgrvtx0  49447  el0ldep  49909  islindeps2  49926  ldepsnlinclem1  49948  ldepsnlinclem2  49949  itscnhlinecirc02plem1  50225  ovconstbrd  50304  ovconstbrn0d  50305  catprs  50456  fucofvalne  50778  tanhneg  51252  crosspv2d  51389  crosspv3d  51390