Theorem eqnetrd 3007

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2939

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  eqnetrrd  3008  3netr4d  3017  opnz  5435  xpdifid  6125  undefne0  8215  onoviun  8294  intrnfi  9361  cantnfp1lem2  9624  cantnfp1lem3  9625  wemapwe  9642  acndom2  9999  fin23lem14  10278  fin23lem40  10296  isf32lem6  10303  isf34lem5  10323  isf34lem7  10324  isf34lem6  10325  axcc2lem  10381  xaddnemnf  13165  xaddnepnf  13166  fseqsupcl  13892  hashprg  14305  elprchashprn2  14306  hash1n0  14331  limsupgre  15375  isercolllem3  15563  prodfn0  15790  ntrivcvgtail  15796  fproddiv  15855  fprodn0  15873  tanval3  16027  tanneg  16041  ruclem11  16133  bezoutr1  16456  phibndlem  16653  dfphi2  16657  0ram  16903  0ram2  16904  ram0  16905  0ramcl  16906  gsumval2  18555  sgrp2nmndlem5  18753  issubg2  18957  ghmrn  19035  pmtrmvd  19252  gsumval3  19698  pgpfaclem2  19875  ablfaclem2  19879  ablfaclem3  19880  fincygsubgodd  19905  subdrgint  20326  abvdom  20353  lbsextlem2  20679  gzrngunit  20900  zringunit  20924  cnmsgnsubg  21018  frlmssuvc2  21238  mhpmulcl  21576  iinopn  22288  cnconn  22810  1stcfb  22833  dissnlocfin  22917  fbasrn  23272  fclscmpi  23417  alexsublem  23432  ustuqtop5  23634  cnextucn  23692  dscmet  23965  reperflem  24218  evth  24359  cmetcaulem  24689  iscmet3  24694  metsscmetcld  24716  cmetss  24717  bcthlem5  24729  bcth2  24731  mbflimsup  25067  itg1addlem4  25100  itg1addlem4OLD  25101  itg1climres  25116  itg2monolem1  25152  itg2i1fseq2  25158  tdeglem4  25461  tdeglem4OLD  25462  deg1add  25505  deg1mul2  25516  deg1tm  25520  dgreq  25642  dgradd2  25666  dgrmul  25668  dgrmulc  25669  dgrcolem1  25671  plyrem  25702  facth  25703  fta1lem  25704  vieta1lem1  25707  vieta1lem2  25708  vieta1  25709  qaa  25720  aareccl  25723  geolim3  25736  aaliou3lem9  25747  coseq00topi  25896  cosne0  25922  tanord  25931  tanarg  26011  cxpne0  26069  cxpsqrt  26095  logbrec  26169  chordthmlem  26219  chordthmlem2  26220  dcubic  26233  mcubic  26234  cubic2  26235  cubic  26236  quartlem4  26247  atandmneg  26293  atandmcj  26296  atancj  26297  atanrecl  26298  atanlogsublem  26302  efiatan2  26304  tanatan  26306  atandmtan  26307  cosatan  26308  cosatanne0  26309  wilthlem2  26455  ftalem7  26465  basellem2  26468  basellem4  26470  basellem5  26471  isppw  26500  dchrptlem2  26650  lgsne0  26720  2sqlem8a  26810  2sqlem8  26811  noseponlem  27049  tglnpt2  27646  midexlem  27697  colperpexlem3  27737  mideulem2  27739  lnopp2hpgb  27768  subgruhgredgd  28295  wwlksnext  28901  wspthsnonn0vne  28925  clwwisshclwws  29022  vdn0conngrumgrv2  29203  vdgn1frgrv2  29303  ifnetrue  31533  ifnefals  31534  imadifxp  31586  acunirnmpt  31642  fnpreimac  31654  xaddeq0  31726  pmtrcnelor  32012  qsidomlem2  32302  madjusmdetlem2  32498  zar0ring  32548  xrge0iifhom  32607  signswn0  33261  signsvtn0  33271  signstfvneq0  33273  repr0  33313  derangenlem  33852  subfacp1lem3  33863  subfacp1lem5  33865  wsuclem  34486  ivthALT  34883  neibastop1  34907  finxpreclem2  35934  finxpreclem6  35940  tan2h  36143  poimirlem9  36160  heicant  36186  itg2addnclem2  36203  lsatfixedN  37544  islshpat  37552  lkrshp  37640  2llnm3N  38105  dalemdnee  38202  cdleme18b  38828  cdleme40m  39003  cdlemg12g  39185  cdlemh  39353  cdlemj3  39359  tendoconid  39365  cdlemk3  39369  cdlemk12  39386  cdlemk12u  39408  cdlemk46  39484  cdlemk54  39494  erngdvlem4  39527  erngdvlem4-rN  39535  dibn0  39689  dihglblem2aN  39829  dochshpncl  39920  dochsnnz  39986  dochsatshpb  39988  lcfl7lem  40035  lcfl8b  40040  lcfrlem33  40111  lcfr  40121  hdmaprnlem3uN  40387  aks4d1p1p7  40604  fldhmf1  40620  metakunt7  40656  ricdrng1  40778  nn0rppwr  40877  remul01  40934  remulinvcom  40959  prjcrv0  41029  3cubeslem2  41066  cmpfiiin  41078  pell1234qrne0  41234  rmxyneg  41302  fnwe2lem2  41436  kelac1  41448  wnefimgd  42556  radcnvrat  42716  binomcxplemfrat  42753  binomcxplemradcnv  42754  disjrnmpt2  43529  disjf1o  43532  choicefi  43542  ioondisj2  43851  ioondisj1  43852  lptioo2  43992  lptioo1  43993  0ellimcdiv  44010  liminflbuz2  44176  ioodvbdlimc1  44294  ioodvbdlimc2  44296  stoweidlem31  44392  stoweidlem59  44420  wallispilem4  44429  wallispi  44431  stirlinglem3  44437  stirlinglem14  44448  dirkerper  44457  dirkertrigeq  44462  dirkercncflem2  44465  fourierdlem4  44472  fourierdlem30  44498  fourierdlem41  44509  fourierdlem42  44510  fourierdlem44  44512  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem62  44529  fourierdlem74  44541  fourierdlem75  44542  fourierdlem79  44546  fourierdlem102  44569  fourierdlem114  44581  fouriersw  44592  elaa2lem  44594  elaa2  44595  etransclem24  44619  etransclem44  44639  etransclem47  44642  ioorrnopnlem  44665  subsaliuncl  44719  sge0cl  44742  meadjun  44823  meadjiunlem  44826  hoicvr  44909  ovnsubadd2lem  45006  smflimlem6  45137  smfpimcc  45169  smflimsuplem2  45182  lswn0  45756  sprvalpwn0  45795  fmtnoprmfac1lem  45876  el0ldep  46667  islindeps2  46684  ldepsnlinclem1  46706  ldepsnlinclem2  46707  itscnhlinecirc02plem1  46988  fvconstr  47042  fvconstrn0  47043  catprs  47151