Theorem eqnetrd 2992

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetrrd  2993  3netr4d  3002  opnz  5433  xpdifid  6141  undefne0  8258  onoviun  8312  intrnfi  9367  cantnfp1lem2  9632  cantnfp1lem3  9633  wemapwe  9650  acndom2  10007  fin23lem14  10286  fin23lem40  10304  isf32lem6  10311  isf34lem5  10331  isf34lem7  10332  isf34lem6  10333  axcc2lem  10389  xaddnemnf  13196  xaddnepnf  13197  fseqsupcl  13942  hashprg  14360  elprchashprn2  14361  hash1n0  14386  limsupgre  15447  isercolllem3  15633  prodfn0  15860  ntrivcvgtail  15866  fproddiv  15927  fprodn0  15945  tanval3  16102  tanneg  16116  ruclem11  16208  nn0rppwr  16531  bezoutr1  16539  phibndlem  16740  dfphi2  16744  0ram  16991  0ram2  16992  ram0  16993  0ramcl  16994  gsumval2  18613  sgrp2nmndlem5  18856  issubg2  19073  ghmrn  19161  pmtrmvd  19386  gsumval3  19837  pgpfaclem2  20014  ablfaclem2  20018  ablfaclem3  20019  fincygsubgodd  20044  subdrgint  20712  abvdom  20739  lbsextlem2  21069  cndrng  21310  gzrngunit  21350  zringunit  21376  cnmsgnsubg  21486  frlmssuvc2  21704  mhpmulcl  22036  iinopn  22789  cnconn  23309  1stcfb  23332  dissnlocfin  23416  fbasrn  23771  fclscmpi  23916  alexsublem  23931  ustuqtop5  24133  cnextucn  24190  dscmet  24460  reperflem  24707  evth  24858  cmetcaulem  25188  iscmet3  25193  metsscmetcld  25215  cmetss  25216  bcthlem5  25228  bcth2  25230  mbflimsup  25567  itg1addlem4  25600  itg1climres  25615  itg2monolem1  25651  itg2i1fseq2  25657  tdeglem4  25965  deg1add  26008  deg1mul2  26019  deg1tm  26024  dgreq  26149  dgradd2  26174  dgrmul  26176  dgrmulc  26177  dgrcolem1  26179  plyrem  26213  facth  26214  fta1lem  26215  vieta1lem1  26218  vieta1lem2  26219  vieta1  26220  qaa  26231  aareccl  26234  geolim3  26247  aaliou3lem9  26258  coseq00topi  26411  cosne0  26438  tanord  26447  tanarg  26528  cxpne0  26586  cxpsqrt  26612  logbrec  26692  chordthmlem  26742  chordthmlem2  26743  dcubic  26756  mcubic  26757  cubic2  26758  cubic  26759  quartlem4  26770  atandmneg  26816  atandmcj  26819  atancj  26820  atanrecl  26821  atanlogsublem  26825  efiatan2  26827  tanatan  26829  atandmtan  26830  cosatan  26831  cosatanne0  26832  wilthlem2  26979  ftalem7  26989  basellem2  26992  basellem4  26994  basellem5  26995  isppw  27024  dchrptlem2  27176  lgsne0  27246  2sqlem8a  27336  2sqlem8  27337  noseponlem  27576  recsne0  28095  tglnpt2  28568  midexlem  28619  colperpexlem3  28659  mideulem2  28661  lnopp2hpgb  28690  subgruhgredgd  29211  wwlksnext  29823  wspthsnonn0vne  29847  clwwisshclwws  29944  vdn0conngrumgrv2  30125  vdgn1frgrv2  30225  nrt2irr  30402  ifnetrue  32476  ifnefals  32477  imadifxp  32530  acunirnmpt  32583  fnpreimac  32595  quad3d  32673  xaddeq0  32676  pmtrcnelor  33048  domnprodn0  33226  qsidomlem2  33424  ply1dg3rt0irred  33551  m1pmeq  33552  ply1annnr  33693  minplyirred  33701  rtelextdg2lem  33716  constrrtcclem  33724  constrconj  33735  constrext2chnlem  33740  constrremulcl  33757  constrrecl  33759  constrreinvcl  33762  2sqr3minply  33770  2sqr3nconstr  33771  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminply  33778  cos9thpinconstrlem1  33779  cos9thpinconstrlem2  33780  cos9thpinconstr  33781  madjusmdetlem2  33818  zar0ring  33868  xrge0iifhom  33927  signswn0  34551  signsvtn0  34561  signstfvneq0  34563  repr0  34602  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  wsuclem  35813  ivthALT  36323  neibastop1  36347  weiunfrlem  36452  finxpreclem2  37378  finxpreclem6  37384  tan2h  37606  poimirlem9  37623  heicant  37649  itg2addnclem2  37666  lsatfixedN  39002  islshpat  39010  lkrshp  39098  2llnm3N  39563  dalemdnee  39660  cdleme18b  40286  cdleme40m  40461  cdlemg12g  40643  cdlemh  40811  cdlemj3  40817  tendoconid  40823  cdlemk3  40827  cdlemk12  40844  cdlemk12u  40866  cdlemk46  40942  cdlemk54  40952  erngdvlem4  40985  erngdvlem4-rN  40993  dibn0  41147  dihglblem2aN  41287  dochshpncl  41378  dochsnnz  41444  dochsatshpb  41446  lcfl7lem  41493  lcfl8b  41498  lcfrlem33  41569  lcfr  41579  hdmaprnlem3uN  41845  aks4d1p1p7  42062  fldhmf1  42078  primrootspoweq0  42094  idomnnzpownz  42120  idomnnzgmulnz  42121  aks6d1c5lem2  42126  deg1gprod  42128  unitscyglem4  42186  tanhalfpim  42337  remul01  42395  remulinvcom  42421  domnexpgn0cl  42511  ricdrng1  42516  prjcrv0  42621  3cubeslem2  42673  cmpfiiin  42685  pell1234qrne0  42841  rmxyneg  42909  fnwe2lem2  43040  kelac1  43052  wnefimgd  44150  radcnvrat  44303  binomcxplemfrat  44340  binomcxplemradcnv  44341  disjrnmpt2  45182  disjf1o  45185  choicefi  45194  ioondisj2  45491  ioondisj1  45492  lptioo2  45629  lptioo1  45630  0ellimcdiv  45647  liminflbuz2  45813  ioodvbdlimc1  45931  ioodvbdlimc2  45933  stoweidlem31  46029  stoweidlem59  46057  wallispilem4  46066  wallispi  46068  stirlinglem3  46074  stirlinglem14  46085  dirkerper  46094  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem4  46109  fourierdlem30  46135  fourierdlem41  46146  fourierdlem42  46147  fourierdlem44  46149  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem62  46166  fourierdlem74  46178  fourierdlem75  46179  fourierdlem79  46183  fourierdlem102  46206  fourierdlem114  46218  fouriersw  46229  elaa2lem  46231  elaa2  46232  etransclem24  46256  etransclem44  46276  etransclem47  46279  ioorrnopnlem  46302  subsaliuncl  46356  sge0cl  46379  meadjun  46460  meadjiunlem  46463  hoicvr  46546  ovnsubadd2lem  46643  smflimlem6  46774  smfpimcc  46806  smflimsuplem2  46819  cjnpoly  46890  modm2nep1  47367  modm1nep2  47369  modm1p1ne  47371  lswn0  47445  sprvalpwn0  47484  fmtnoprmfac1lem  47565  grimuhgr  47887  gpg3nbgrvtx0  48067  el0ldep  48455  islindeps2  48472  ldepsnlinclem1  48494  ldepsnlinclem2  48495  itscnhlinecirc02plem1  48771  fvconstr  48850  fvconstrn0  48851  catprs  49000  fucofvalne  49314