Theorem eqnetrd 3025

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  eqnetrrd  3026  3netr4d  3035  opnz  5457  xpdifid  6167  undefne0  8277  onoviun  8331  intrnfi  9377  cantnfp1lem2  9649  cantnfp1lem3  9650  wemapwe  9667  acndom2  10039  fin23lem14  10318  fin23lem40  10336  isf32lem6  10343  isf34lem5  10363  isf34lem7  10364  isf34lem6  10365  axcc2lem  10421  xaddnemnf  13263  xaddnepnf  13264  fseqsupcl  14015  hashprg  14433  elprchashprn2  14434  hash1n0  14460  limsupgre  15534  isercolllem3  15720  prodfn0  15950  ntrivcvgtail  15956  fproddiv  16017  fprodn0  16035  tanval3  16191  tanneg  16205  ruclem11  16297  nn0rppwr  16620  bezoutr1  16628  phibndlem  16830  dfphi2  16834  0ram  17081  0ram2  17082  ram0  17083  0ramcl  17084  gsumval2  18745  sgrp2nmndlem5  18992  issubg2  19209  ghmrn  19300  pmtrmvd  19527  gsumval3  19978  pgpfaclem2  20155  ablfaclem2  20159  ablfaclem3  20160  fincygsubgodd  20185  subdrgint  20887  abvdom  20914  lbsextlem2  21264  qsidomlem2  21462  cndrng  21532  gzrngunit  21564  zringunit  21597  cnmsgnsubg  21708  frlmssuvc2  21926  mhpmulcl  22293  iinopn  23040  cnconn  23560  1stcfb  23583  dissnlocfin  23667  fbasrn  24022  fclscmpi  24167  alexsublem  24182  ustuqtop5  24383  cnextucn  24440  dscmet  24710  reperflem  24957  evth  25099  cmetcaulem  25428  iscmet3  25433  metsscmetcld  25455  cmetss  25456  bcthlem5  25468  bcth2  25470  mbflimsup  25806  itg1addlem4  25839  itg1climres  25854  itg2monolem1  25890  itg2i1fseq2  25896  tdeglem4  26198  deg1add  26241  deg1mul2  26252  deg1tm  26257  dgreq  26382  dgradd2  26406  dgrmul  26408  dgrmulc  26409  dgrcolem1  26411  plyrem  26447  facth  26448  fta1lem  26449  vieta1lem1  26452  vieta1lem2  26453  vieta1  26454  qaa  26465  aareccl  26470  geolim3  26483  aaliou3lem9  26494  coseq00topi  26648  cosne0  26675  tanord  26684  tanarg  26765  cxpne0  26823  cxpsqrt  26849  logbrec  26928  chordthmlem  26978  chordthmlem2  26979  dcubic  26992  mcubic  26993  cubic2  26994  cubic  26995  quartlem4  27006  atandmneg  27052  atandmcj  27055  atancj  27056  atanrecl  27057  atanlogsublem  27061  efiatan2  27063  tanatan  27065  atandmtan  27066  cosatan  27067  cosatanne0  27068  wilthlem2  27214  ftalem7  27224  basellem2  27227  basellem4  27229  basellem5  27230  isppw  27259  dchrptlem2  27410  lgsne0  27480  2sqlem8a  27570  2sqlem8  27571  noseponlem  27809  recsne0  28366  tglnpt2  28907  midexlem  28950  colperpexlem3  28994  mideulem2  28996  lnopp2hpgb  29026  subgruhgredgd  29615  wwlksnext  30223  wspthsnonn0vne  30247  clwwisshclwws  30347  vdn0conngrumgrv2  30528  vdgn1frgrv2  30628  nrt2irr  30805  ifnetrue  32874  ifnefals  32875  imadifxp  32927  acunirnmpt  32985  fnpreimac  32996  quad3d  33075  xaddeq0  33079  pmtrcnelor  33392  domnprodn0  33579  domnprodeq0  33580  drnglring  33763  dflringlem3  33767  dflring4  33769  ply1dg3rt0irred  33855  m1pmeq  33856  mplmulmvr  33910  esplyfvaln  33945  esplyind  33946  ply1annnr  34074  minplyirred  34082  rtelextdg2lem  34097  constrrtcclem  34105  constrconj  34116  constrext2chnlem  34121  constrremulcl  34138  constrrecl  34140  constrreinvcl  34143  2sqr3minply  34151  2sqr3nconstr  34152  cos9thpiminplylem1  34153  cos9thpiminplylem2  34154  cos9thpiminplylem3  34155  cos9thpiminply  34159  cos9thpinconstrlem1  34160  cos9thpinconstrlem2  34161  cos9thpinconstr  34162  madjusmdetlem2  34199  zar0ring  34249  xrge0iifhom  34308  signswn0  34928  signsvtn0  34938  signstfvneq0  34940  repr0  34979  kard0b  35553  derangenlem  35644  subfacp1lem3  35655  subfacp1lem5  35657  wsuclem  36296  ivthALT  36827  neibastop1  36851  weiunfrlem  36956  finxpreclem2  38017  finxpreclem6  38023  tan2h  38244  poimirlem9  38261  heicant  38287  itg2addnclem2  38304  lsatfixedN  39764  islshpat  39772  lkrshp  39860  2llnm3N  40324  dalemdnee  40421  cdleme18b  41047  cdleme40m  41222  cdlemg12g  41404  cdlemh  41572  cdlemj3  41578  tendoconid  41584  cdlemk3  41588  cdlemk12  41605  cdlemk12u  41627  cdlemk46  41703  cdlemk54  41713  erngdvlem4  41746  erngdvlem4-rN  41754  dibn0  41908  dihglblem2aN  42048  dochshpncl  42139  dochsnnz  42205  dochsatshpb  42207  lcfl7lem  42254  lcfl8b  42259  lcfrlem33  42330  lcfr  42340  hdmaprnlem3uN  42606  aks4d1p1p7  42822  fldhmf1  42838  primrootspoweq0  42854  idomnnzpownz  42880  idomnnzgmulnz  42881  aks6d1c5lem2  42886  deg1gprod  42888  unitscyglem4  42946  25or6to4  42954  tanhalfpim  43091  remul01  43149  remulinvcom  43175  domnexpgn0cl  43274  ricdrng1  43279  prjcrv0  43348  3cubeslem2  43399  cmpfiiin  43411  pell1234qrne0  43563  rmxyneg  43630  fnwe2lem2  43761  kelac1  43773  wnefimgd  44870  radcnvrat  45007  binomcxplemfrat  45044  binomcxplemradcnv  45045  disjrnmpt2  45889  disjf1o  45892  choicefi  45900  ioondisj2  46192  ioondisj1  46193  lptioo2  46330  lptioo1  46331  0ellimcdiv  46346  liminflbuz2  46512  ioodvbdlimc1  46630  ioodvbdlimc2  46632  stoweidlem31  46728  stoweidlem59  46756  wallispilem4  46765  wallispi  46767  stirlinglem3  46773  stirlinglem14  46784  dirkerper  46793  dirkertrigeq  46798  dirkercncflem2  46801  fourierdlem4  46808  fourierdlem30  46834  fourierdlem41  46845  fourierdlem42  46846  fourierdlem44  46848  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem62  46865  fourierdlem74  46877  fourierdlem75  46878  fourierdlem79  46882  fourierdlem102  46905  fourierdlem114  46917  fouriersw  46928  elaa2lem  46930  elaa2  46931  etransclem24  46955  etransclem44  46975  etransclem47  46978  ioorrnopnlem  47001  subsaliuncl  47055  sge0cl  47078  meadjun  47159  meadjiunlem  47162  hoicvr  47245  ovnsubadd2lem  47342  smflimlem6  47473  smfpimcc  47505  smflimsuplem2  47518  sqrtnnaa  47587  sqrtnzqaa  47588  cjnpoly  47609  modm2nep1  48092  modm1nep2  48094  modm1p1ne  48096  lswn0  48176  sprvalpwn0  48215  fmtnoprmfac1lem  48299  grimuhgr  48635  gpg3nbgrvtx0  48824  el0ldep  49229  islindeps2  49246  ldepsnlinclem1  49268  ldepsnlinclem2  49269  itscnhlinecirc02plem1  49545  fvconstr  49623  fvconstrn0  49624  catprs  49772  fucofvalne  50086