Theorem eqnetrd 3054

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

Syntax hints:   → wi 4   = wceq 1538   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  eqnetrrd  3055  3netr4d  3064  opnz  5330  xpdifid  5992  undefne0  7928  onoviun  7963  intrnfi  8864  cantnfp1lem2  9126  cantnfp1lem3  9127  wemapwe  9144  acndom2  9465  fin23lem14  9744  fin23lem40  9762  isf32lem6  9769  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  axcc2lem  9847  xaddnemnf  12617  xaddnepnf  12618  fseqsupcl  13340  hashprg  13752  elprchashprn2  13753  hash1n0  13778  limsupgre  14830  isercolllem3  15015  prodfn0  15242  ntrivcvgtail  15248  fproddiv  15307  fprodn0  15325  tanval3  15479  tanneg  15493  ruclem11  15585  bezoutr1  15903  phibndlem  16097  dfphi2  16101  0ram  16346  0ram2  16347  ram0  16348  0ramcl  16349  gsumval2  17888  sgrp2nmndlem5  18086  issubg2  18286  ghmrn  18363  pmtrmvd  18576  gsumval3  19020  pgpfaclem2  19197  ablfaclem2  19201  ablfaclem3  19202  fincygsubgodd  19227  subdrgint  19575  abvdom  19602  lbsextlem2  19924  gzrngunit  20157  zringunit  20181  cnmsgnsubg  20266  frlmssuvc2  20484  iinopn  21507  cnconn  22027  1stcfb  22050  dissnlocfin  22134  fbasrn  22489  fclscmpi  22634  alexsublem  22649  ustuqtop5  22851  cnextucn  22909  dscmet  23179  reperflem  23423  evth  23564  cmetcaulem  23892  iscmet3  23897  metsscmetcld  23919  cmetss  23920  bcthlem5  23932  bcth2  23934  mbflimsup  24270  itg1addlem4  24303  itg1climres  24318  itg2monolem1  24354  itg2i1fseq2  24360  tdeglem4  24661  deg1add  24704  deg1mul2  24715  deg1tm  24719  dgreq  24841  dgradd2  24865  dgrmul  24867  dgrmulc  24868  dgrcolem1  24870  plyrem  24901  facth  24902  fta1lem  24903  vieta1lem1  24906  vieta1lem2  24907  vieta1  24908  qaa  24919  aareccl  24922  geolim3  24935  aaliou3lem9  24946  coseq00topi  25095  cosne0  25121  tanord  25130  tanarg  25210  cxpne0  25268  cxpsqrt  25294  logbrec  25368  chordthmlem  25418  chordthmlem2  25419  dcubic  25432  mcubic  25433  cubic2  25434  cubic  25435  quartlem4  25446  atandmneg  25492  atandmcj  25495  atancj  25496  atanrecl  25497  atanlogsublem  25501  efiatan2  25503  tanatan  25505  atandmtan  25506  cosatan  25507  cosatanne0  25508  wilthlem2  25654  ftalem7  25664  basellem2  25667  basellem4  25669  basellem5  25670  isppw  25699  dchrptlem2  25849  lgsne0  25919  2sqlem8a  26009  2sqlem8  26010  tglnpt2  26435  midexlem  26486  colperpexlem3  26526  mideulem2  26528  lnopp2hpgb  26557  subgruhgredgd  27074  wwlksnext  27679  wspthsnonn0vne  27703  clwwisshclwws  27800  vdn0conngrumgrv2  27981  vdgn1frgrv2  28081  imadifxp  30364  acunirnmpt  30422  fnpreimac  30434  xaddeq0  30503  pmtrcnelor  30785  qsidomlem2  31037  madjusmdetlem2  31181  zar0ring  31231  xrge0iifhom  31290  signswn0  31940  signsvtn0  31950  signstfvneq0  31952  repr0  31992  derangenlem  32531  subfacp1lem3  32542  subfacp1lem5  32544  wsuclem  33225  noseponlem  33284  ivthALT  33796  neibastop1  33820  finxpreclem2  34807  finxpreclem6  34813  tan2h  35049  poimirlem9  35066  heicant  35092  itg2addnclem2  35109  lsatfixedN  36305  islshpat  36313  lkrshp  36401  2llnm3N  36865  dalemdnee  36962  cdleme18b  37588  cdleme40m  37763  cdlemg12g  37945  cdlemh  38113  cdlemj3  38119  tendoconid  38125  cdlemk3  38129  cdlemk12  38146  cdlemk12u  38168  cdlemk46  38244  cdlemk54  38254  erngdvlem4  38287  erngdvlem4-rN  38295  dibn0  38449  dihglblem2aN  38589  dochshpncl  38680  dochsnnz  38746  dochsatshpb  38748  lcfl7lem  38795  lcfl8b  38800  lcfrlem33  38871  lcfr  38881  hdmaprnlem3uN  39147  metakunt7  39356  nn0rppwr  39490  remul01  39545  remulinvcom  39569  3cubeslem2  39626  cmpfiiin  39638  pell1234qrne0  39794  rmxyneg  39861  fnwe2lem2  39995  kelac1  40007  wnefimgd  40865  radcnvrat  41018  binomcxplemfrat  41055  binomcxplemradcnv  41056  disjrnmpt2  41815  disjf1o  41818  choicefi  41829  ioondisj2  42130  ioondisj1  42131  lptioo2  42273  lptioo1  42274  0ellimcdiv  42291  liminflbuz2  42457  ioodvbdlimc1  42575  ioodvbdlimc2  42577  stoweidlem31  42673  stoweidlem59  42701  wallispilem4  42710  wallispi  42712  stirlinglem3  42718  stirlinglem14  42729  dirkerper  42738  dirkertrigeq  42743  dirkercncflem2  42746  fourierdlem4  42753  fourierdlem30  42779  fourierdlem41  42790  fourierdlem42  42791  fourierdlem44  42793  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem62  42810  fourierdlem74  42822  fourierdlem75  42823  fourierdlem79  42827  fourierdlem102  42850  fourierdlem114  42862  fouriersw  42873  elaa2lem  42875  elaa2  42876  etransclem24  42900  etransclem44  42920  etransclem47  42923  ioorrnopnlem  42946  subsaliuncl  42998  sge0cl  43020  meadjun  43101  meadjiunlem  43104  hoicvr  43187  ovnsubadd2lem  43284  smflimlem6  43409  smfpimcc  43439  smflimsuplem2  43452  lswn0  43961  sprvalpwn0  44000  fmtnoprmfac1lem  44081  el0ldep  44875  islindeps2  44892  ldepsnlinclem1  44914  ldepsnlinclem2  44915  itscnhlinecirc02plem1  45196