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  5420  xpdifid  6121  undefne0  8219  onoviun  8273  intrnfi  9325  cantnfp1lem2  9594  cantnfp1lem3  9595  wemapwe  9612  acndom2  9967  fin23lem14  10246  fin23lem40  10264  isf32lem6  10271  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axcc2lem  10349  xaddnemnf  13157  xaddnepnf  13158  fseqsupcl  13903  hashprg  14321  elprchashprn2  14322  hash1n0  14347  limsupgre  15407  isercolllem3  15593  prodfn0  15820  ntrivcvgtail  15826  fproddiv  15887  fprodn0  15905  tanval3  16062  tanneg  16076  ruclem11  16168  nn0rppwr  16491  bezoutr1  16499  phibndlem  16700  dfphi2  16704  0ram  16951  0ram2  16952  ram0  16953  0ramcl  16954  gsumval2  18579  sgrp2nmndlem5  18822  issubg2  19039  ghmrn  19127  pmtrmvd  19354  gsumval3  19805  pgpfaclem2  19982  ablfaclem2  19986  ablfaclem3  19987  fincygsubgodd  20012  subdrgint  20707  abvdom  20734  lbsextlem2  21085  cndrng  21324  gzrngunit  21359  zringunit  21392  cnmsgnsubg  21503  frlmssuvc2  21721  mhpmulcl  22053  iinopn  22806  cnconn  23326  1stcfb  23349  dissnlocfin  23433  fbasrn  23788  fclscmpi  23933  alexsublem  23948  ustuqtop5  24150  cnextucn  24207  dscmet  24477  reperflem  24724  evth  24875  cmetcaulem  25205  iscmet3  25210  metsscmetcld  25232  cmetss  25233  bcthlem5  25245  bcth2  25247  mbflimsup  25584  itg1addlem4  25617  itg1climres  25632  itg2monolem1  25668  itg2i1fseq2  25674  tdeglem4  25982  deg1add  26025  deg1mul2  26036  deg1tm  26041  dgreq  26166  dgradd2  26191  dgrmul  26193  dgrmulc  26194  dgrcolem1  26196  plyrem  26230  facth  26231  fta1lem  26232  vieta1lem1  26235  vieta1lem2  26236  vieta1  26237  qaa  26248  aareccl  26251  geolim3  26264  aaliou3lem9  26275  coseq00topi  26428  cosne0  26455  tanord  26464  tanarg  26545  cxpne0  26603  cxpsqrt  26629  logbrec  26709  chordthmlem  26759  chordthmlem2  26760  dcubic  26773  mcubic  26774  cubic2  26775  cubic  26776  quartlem4  26787  atandmneg  26833  atandmcj  26836  atancj  26837  atanrecl  26838  atanlogsublem  26842  efiatan2  26844  tanatan  26846  atandmtan  26847  cosatan  26848  cosatanne0  26849  wilthlem2  26996  ftalem7  27006  basellem2  27009  basellem4  27011  basellem5  27012  isppw  27041  dchrptlem2  27193  lgsne0  27263  2sqlem8a  27353  2sqlem8  27354  noseponlem  27593  recsne0  28119  tglnpt2  28605  midexlem  28656  colperpexlem3  28696  mideulem2  28698  lnopp2hpgb  28727  subgruhgredgd  29248  wwlksnext  29857  wspthsnonn0vne  29881  clwwisshclwws  29978  vdn0conngrumgrv2  30159  vdgn1frgrv2  30259  nrt2irr  30436  ifnetrue  32510  ifnefals  32511  imadifxp  32564  acunirnmpt  32621  fnpreimac  32633  quad3d  32712  xaddeq0  32715  pmtrcnelor  33052  domnprodn0  33234  qsidomlem2  33409  ply1dg3rt0irred  33537  m1pmeq  33538  ply1annnr  33689  minplyirred  33697  rtelextdg2lem  33712  constrrtcclem  33720  constrconj  33731  constrext2chnlem  33736  constrremulcl  33753  constrrecl  33755  constrreinvcl  33758  2sqr3minply  33766  2sqr3nconstr  33767  cos9thpiminplylem1  33768  cos9thpiminplylem2  33769  cos9thpiminplylem3  33770  cos9thpiminply  33774  cos9thpinconstrlem1  33775  cos9thpinconstrlem2  33776  cos9thpinconstr  33777  madjusmdetlem2  33814  zar0ring  33864  xrge0iifhom  33923  signswn0  34547  signsvtn0  34557  signstfvneq0  34559  repr0  34598  derangenlem  35163  subfacp1lem3  35174  subfacp1lem5  35176  wsuclem  35818  ivthALT  36328  neibastop1  36352  weiunfrlem  36457  finxpreclem2  37383  finxpreclem6  37389  tan2h  37611  poimirlem9  37628  heicant  37654  itg2addnclem2  37671  lsatfixedN  39007  islshpat  39015  lkrshp  39103  2llnm3N  39568  dalemdnee  39665  cdleme18b  40291  cdleme40m  40466  cdlemg12g  40648  cdlemh  40816  cdlemj3  40822  tendoconid  40828  cdlemk3  40832  cdlemk12  40849  cdlemk12u  40871  cdlemk46  40947  cdlemk54  40957  erngdvlem4  40990  erngdvlem4-rN  40998  dibn0  41152  dihglblem2aN  41292  dochshpncl  41383  dochsnnz  41449  dochsatshpb  41451  lcfl7lem  41498  lcfl8b  41503  lcfrlem33  41574  lcfr  41584  hdmaprnlem3uN  41850  aks4d1p1p7  42067  fldhmf1  42083  primrootspoweq0  42099  idomnnzpownz  42125  idomnnzgmulnz  42126  aks6d1c5lem2  42131  deg1gprod  42133  unitscyglem4  42191  tanhalfpim  42342  remul01  42400  remulinvcom  42426  domnexpgn0cl  42516  ricdrng1  42521  prjcrv0  42626  3cubeslem2  42678  cmpfiiin  42690  pell1234qrne0  42846  rmxyneg  42913  fnwe2lem2  43044  kelac1  43056  wnefimgd  44154  radcnvrat  44307  binomcxplemfrat  44344  binomcxplemradcnv  44345  disjrnmpt2  45186  disjf1o  45189  choicefi  45198  ioondisj2  45494  ioondisj1  45495  lptioo2  45632  lptioo1  45633  0ellimcdiv  45650  liminflbuz2  45816  ioodvbdlimc1  45934  ioodvbdlimc2  45936  stoweidlem31  46032  stoweidlem59  46060  wallispilem4  46069  wallispi  46071  stirlinglem3  46077  stirlinglem14  46088  dirkerper  46097  dirkertrigeq  46102  dirkercncflem2  46105  fourierdlem4  46112  fourierdlem30  46138  fourierdlem41  46149  fourierdlem42  46150  fourierdlem44  46152  fourierdlem46  46153  fourierdlem48  46155  fourierdlem49  46156  fourierdlem62  46169  fourierdlem74  46181  fourierdlem75  46182  fourierdlem79  46186  fourierdlem102  46209  fourierdlem114  46221  fouriersw  46232  elaa2lem  46234  elaa2  46235  etransclem24  46259  etransclem44  46279  etransclem47  46282  ioorrnopnlem  46305  subsaliuncl  46359  sge0cl  46382  meadjun  46463  meadjiunlem  46466  hoicvr  46549  ovnsubadd2lem  46646  smflimlem6  46777  smfpimcc  46809  smflimsuplem2  46822  cjnpoly  46893  modm2nep1  47370  modm1nep2  47372  modm1p1ne  47374  lswn0  47448  sprvalpwn0  47487  fmtnoprmfac1lem  47568  grimuhgr  47891  gpg3nbgrvtx0  48080  el0ldep  48471  islindeps2  48488  ldepsnlinclem1  48510  ldepsnlinclem2  48511  itscnhlinecirc02plem1  48787  fvconstr  48866  fvconstrn0  48867  catprs  49016  fucofvalne  49330