Theorem eqnetrd 3031

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  eqnetrrd  3032  3netr4d  3041  opnz  5453  xpdifid  6164  undefne0  8272  onoviun  8326  intrnfi  9372  cantnfp1lem2  9644  cantnfp1lem3  9645  wemapwe  9662  acndom2  10034  fin23lem14  10313  fin23lem40  10331  isf32lem6  10338  isf34lem5  10358  isf34lem7  10359  isf34lem6  10360  axcc2lem  10416  xaddnemnf  13258  xaddnepnf  13259  fseqsupcl  14009  hashprg  14427  elprchashprn2  14428  hash1n0  14454  limsupgre  15528  isercolllem3  15714  prodfn0  15944  ntrivcvgtail  15950  fproddiv  16011  fprodn0  16029  tanval3  16186  tanneg  16200  ruclem11  16292  nn0rppwr  16615  bezoutr1  16623  phibndlem  16825  dfphi2  16829  0ram  17076  0ram2  17077  ram0  17078  0ramcl  17079  gsumval2  18740  sgrp2nmndlem5  18987  issubg2  19204  ghmrn  19295  pmtrmvd  19522  gsumval3  19973  pgpfaclem2  20150  ablfaclem2  20154  ablfaclem3  20155  fincygsubgodd  20180  subdrgint  20880  abvdom  20907  lbsextlem2  21257  qsidomlem2  21446  cndrng  21516  gzrngunit  21548  zringunit  21581  cnmsgnsubg  21692  frlmssuvc2  21910  mhpmulcl  22277  iinopn  23024  cnconn  23544  1stcfb  23567  dissnlocfin  23651  fbasrn  24006  fclscmpi  24151  alexsublem  24166  ustuqtop5  24367  cnextucn  24424  dscmet  24694  reperflem  24941  evth  25083  cmetcaulem  25412  iscmet3  25417  metsscmetcld  25439  cmetss  25440  bcthlem5  25452  bcth2  25454  mbflimsup  25790  itg1addlem4  25823  itg1climres  25838  itg2monolem1  25874  itg2i1fseq2  25880  tdeglem4  26182  deg1add  26225  deg1mul2  26236  deg1tm  26241  dgreq  26366  dgradd2  26390  dgrmul  26392  dgrmulc  26393  dgrcolem1  26395  plyrem  26431  facth  26432  fta1lem  26433  vieta1lem1  26436  vieta1lem2  26437  vieta1  26438  qaa  26449  aareccl  26452  geolim3  26465  aaliou3lem9  26476  coseq00topi  26629  cosne0  26656  tanord  26665  tanarg  26746  cxpne0  26804  cxpsqrt  26830  logbrec  26909  chordthmlem  26959  chordthmlem2  26960  dcubic  26973  mcubic  26974  cubic2  26975  cubic  26976  quartlem4  26987  atandmneg  27033  atandmcj  27036  atancj  27037  atanrecl  27038  atanlogsublem  27042  efiatan2  27044  tanatan  27046  atandmtan  27047  cosatan  27048  cosatanne0  27049  wilthlem2  27195  ftalem7  27205  basellem2  27208  basellem4  27210  basellem5  27211  isppw  27240  dchrptlem2  27391  lgsne0  27461  2sqlem8a  27551  2sqlem8  27552  noseponlem  27790  recsne0  28347  tglnpt2  28884  midexlem  28927  colperpexlem3  28968  mideulem2  28970  lnopp2hpgb  29000  subgruhgredgd  29571  wwlksnext  30179  wspthsnonn0vne  30203  clwwisshclwws  30303  vdn0conngrumgrv2  30484  vdgn1frgrv2  30584  nrt2irr  30761  ifnetrue  32830  ifnefals  32831  imadifxp  32883  acunirnmpt  32941  fnpreimac  32952  quad3d  33031  xaddeq0  33035  pmtrcnelor  33348  domnprodn0  33535  domnprodeq0  33536  drnglring  33723  dflringlem3  33727  dflring4  33729  ply1dg3rt0irred  33815  m1pmeq  33816  mplmulmvr  33870  esplyfvaln  33905  esplyind  33906  ply1annnr  34034  minplyirred  34042  rtelextdg2lem  34057  constrrtcclem  34065  constrconj  34076  constrext2chnlem  34081  constrremulcl  34098  constrrecl  34100  constrreinvcl  34103  2sqr3minply  34111  2sqr3nconstr  34112  cos9thpiminplylem1  34113  cos9thpiminplylem2  34114  cos9thpiminplylem3  34115  cos9thpiminply  34119  cos9thpinconstrlem1  34120  cos9thpinconstrlem2  34121  cos9thpinconstr  34122  madjusmdetlem2  34159  zar0ring  34209  xrge0iifhom  34268  signswn0  34888  signsvtn0  34898  signstfvneq0  34900  repr0  34939  derangenlem  35558  subfacp1lem3  35569  subfacp1lem5  35571  wsuclem  36210  ivthALT  36731  neibastop1  36755  weiunfrlem  36860  finxpreclem2  37919  finxpreclem6  37925  tan2h  38146  poimirlem9  38163  heicant  38189  itg2addnclem2  38206  lsatfixedN  39668  islshpat  39676  lkrshp  39764  2llnm3N  40228  dalemdnee  40325  cdleme18b  40951  cdleme40m  41126  cdlemg12g  41308  cdlemh  41476  cdlemj3  41482  tendoconid  41488  cdlemk3  41492  cdlemk12  41509  cdlemk12u  41531  cdlemk46  41607  cdlemk54  41617  erngdvlem4  41650  erngdvlem4-rN  41658  dibn0  41812  dihglblem2aN  41952  dochshpncl  42043  dochsnnz  42109  dochsatshpb  42111  lcfl7lem  42158  lcfl8b  42163  lcfrlem33  42234  lcfr  42244  hdmaprnlem3uN  42510  aks4d1p1p7  42726  fldhmf1  42742  primrootspoweq0  42758  idomnnzpownz  42784  idomnnzgmulnz  42785  aks6d1c5lem2  42790  deg1gprod  42792  unitscyglem4  42850  tanhalfpim  42993  remul01  43051  remulinvcom  43077  domnexpgn0cl  43176  ricdrng1  43181  prjcrv0  43250  3cubeslem2  43301  cmpfiiin  43313  pell1234qrne0  43465  rmxyneg  43532  fnwe2lem2  43663  kelac1  43675  wnefimgd  44772  radcnvrat  44909  binomcxplemfrat  44946  binomcxplemradcnv  44947  disjrnmpt2  45791  disjf1o  45794  choicefi  45802  ioondisj2  46094  ioondisj1  46095  lptioo2  46232  lptioo1  46233  0ellimcdiv  46248  liminflbuz2  46414  ioodvbdlimc1  46532  ioodvbdlimc2  46534  stoweidlem31  46630  stoweidlem59  46658  wallispilem4  46667  wallispi  46669  stirlinglem3  46675  stirlinglem14  46686  dirkerper  46695  dirkertrigeq  46700  dirkercncflem2  46703  fourierdlem4  46710  fourierdlem30  46736  fourierdlem41  46747  fourierdlem42  46748  fourierdlem44  46750  fourierdlem46  46751  fourierdlem48  46753  fourierdlem49  46754  fourierdlem62  46767  fourierdlem74  46779  fourierdlem75  46780  fourierdlem79  46784  fourierdlem102  46807  fourierdlem114  46819  fouriersw  46830  elaa2lem  46832  elaa2  46833  etransclem24  46857  etransclem44  46877  etransclem47  46880  ioorrnopnlem  46903  subsaliuncl  46957  sge0cl  46980  meadjun  47061  meadjiunlem  47064  hoicvr  47147  ovnsubadd2lem  47244  smflimlem6  47375  smfpimcc  47407  smflimsuplem2  47420  cjnpoly  47508  modm2nep1  47991  modm1nep2  47993  modm1p1ne  47995  lswn0  48075  sprvalpwn0  48114  fmtnoprmfac1lem  48198  grimuhgr  48534  gpg3nbgrvtx0  48723  el0ldep  49124  islindeps2  49141  ldepsnlinclem1  49163  ldepsnlinclem2  49164  itscnhlinecirc02plem1  49440  fvconstr  49518  fvconstrn0  49519  catprs  49667  fucofvalne  49981