Theorem eqnetrd 3022

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  eqnetrrd  3023  3netr4d  3032  opnz  5441  xpdifid  6158  undefne0  8301  onoviun  8355  intrnfi  9412  cantnfp1lem2  9684  cantnfp1lem3  9685  wemapwe  9702  acndom2  10137  fin23lem14  10415  fin23lem40  10433  isf32lem6  10440  isf34lem5  10460  isf34lem7  10461  isf34lem6  10462  axcc2lem  10518  xaddnemnf  13370  xaddnepnf  13371  fseqsupcl  14124  hashprg  14543  elprchashprn2  14544  hash1n0  14570  limsupgre  15654  isercolllem3  15840  prodfn0  16069  ntrivcvgtail  16075  fproddiv  16134  fprodn0  16152  tanval3  16308  tanneg  16322  ruclem11  16414  nn0rppwr  16741  bezoutr1  16750  phibndlem  16953  dfphi2  16957  0ram  17204  0ram2  17205  ram0  17206  0ramcl  17207  gsumval2  18881  sgrp2nmndlem5  19134  issubg2  19358  ghmrn  19449  pmtrmvd  19676  gsumval3  20127  pgpfaclem2  20304  ablfaclem2  20308  ablfaclem3  20309  fincygsubgodd  20334  subdrgint  21066  abvdom  21093  lbsextlem2  21443  qsidomlem2  21643  cndrng  21713  gzrngunit  21745  zringunit  21778  cnmsgnsubg  21889  frlmssuvc2  22107  mhpmulcl  22476  iinopn  23226  cnconn  23746  1stcfb  23769  dissnlocfin  23854  fbasrn  24209  fclscmpi  24354  alexsublem  24369  ustuqtop5  24570  cnextucn  24627  dscmet  24897  reperflem  25144  evth  25286  cmetcaulem  25615  iscmet3  25620  metsscmetcld  25642  cmetss  25643  bcthlem5  25655  bcth2  25657  mbflimsup  25993  itg1addlem4  26026  itg1climres  26041  itg2monolem1  26077  itg2i1fseq2  26083  tdeglem4  26384  deg1add  26427  deg1mul2  26438  deg1tm  26443  dgreq  26569  dgradd2  26593  dgrmul  26595  dgrmulc  26596  dgrcolem1  26598  plyrem  26632  facth  26633  fta1lem  26634  vieta1lem1  26639  vieta1lem2  26640  vieta1  26641  qaa  26653  aareccl  26659  geolim3  26672  aaliou3lem9  26683  coseq00topi  26837  cosne0  26863  tanord  26872  tanarg  26953  cxpne0  27011  cxpsqrt  27037  logbrec  27116  chordthmlem  27166  chordthmlem2  27167  dcubic  27180  mcubic  27181  cubic2  27182  cubic  27183  quartlem4  27194  atandmneg  27240  atandmcj  27243  atancj  27244  atanrecl  27245  atanlogsublem  27249  efiatan2  27251  tanatan  27253  atandmtan  27254  cosatan  27255  cosatanne0  27256  wilthlem2  27402  ftalem7  27412  basellem2  27415  basellem4  27417  basellem5  27418  isppw  27447  dchrptlem2  27598  lgsne0  27668  2sqlem8a  27758  2sqlem8  27759  noseponlem  28027  recsne0  28584  tglnpt2  29127  midexlem  29170  colperpexlem3  29214  mideulem2  29216  lnopp2hpgb  29247  angmgmaddov1  29394  subgruhgredgd  29871  wwlksnext  30488  wspthsnonn0vne  30512  clwwisshclwws  30612  vdn0conngrumgrv2  30803  vdgn1frgrv2  30903  nrt2irr  31080  tgextamirnhl  33078  ifnetrue  33191  ifnefals  33192  imadifxp  33243  acunirnmpt  33301  fnpreimac  33312  quad3d  33388  xaddeq0  33392  pmtrcnelor  33699  domnprodn0  33886  domnprodeq0  33887  drnglring  34071  dflringlem3  34075  dflring4  34077  ply1dg3rt0irred  34163  m1pmeq  34164  mplmulmvr  34218  esplyfvaln  34253  esplyind  34254  ply1annnr  34382  minplyirred  34390  rtelextdg2lem  34405  constrrtcclem  34413  constrconj  34424  constrext2chnlem  34429  constrremulcl  34446  constrrecl  34448  constrreinvcl  34451  2sqr3minply  34459  2sqr3nconstr  34460  cos9thpiminplylem1  34461  cos9thpiminplylem2  34462  cos9thpiminplylem3  34463  cos9thpiminply  34467  cos9thpinconstrlem1  34468  cos9thpinconstrlem2  34469  cos9thpinconstr  34470  madjusmdetlem2  34507  zar0ring  34557  xrge0iifhom  34616  signswn0  35236  signsvtn0  35246  signstfvneq0  35248  repr0  35287  kard0b  35884  derangenlem  36023  subfacp1lem3  36034  subfacp1lem5  36036  wsuclem  36680  ivthALT  37216  neibastop1  37240  weiunfrlem  37345  mh-inf3f1  37422  finxpreclem2  38407  finxpreclem6  38413  tan2h  38629  poimirlem9  38641  heicant  38667  itg2addnclem2  38684  lsatfixedN  40160  islshpat  40168  lkrshp  40256  2llnm3N  40720  dalemdnee  40817  cdleme18b  41443  cdleme40m  41618  cdlemg12g  41800  cdlemh  41968  cdlemj3  41974  tendoconid  41980  cdlemk3  41984  cdlemk12  42001  cdlemk12u  42023  cdlemk46  42099  cdlemk54  42109  erngdvlem4  42142  erngdvlem4-rN  42150  dibn0  42304  dihglblem2aN  42444  dochshpncl  42535  dochsnnz  42601  dochsatshpb  42603  lcfl7lem  42650  lcfl8b  42655  lcfrlem33  42726  lcfr  42736  hdmaprnlem3uN  43002  aks4d1p1p7  43218  fldhmf1  43234  primrootspoweq0  43250  idomnnzpownz  43276  idomnnzgmulnz  43277  aks6d1c5lem2  43282  deg1gprod  43284  unitscyglem4  43342  25or6to4  43350  tanhalfpim  43494  remul01  43552  remulinvcom  43578  domnexpgn0cl  43678  ricdrng1  43686  prjcrv0  43763  3cubeslem2  43789  cmpfiiin  43802  pell1234qrne0  43954  rmxyneg  44021  kelac1  44159  wnefimgd  45255  radcnvrat  45392  binomcxplemfrat  45429  binomcxplemradcnv  45430  disjrnmpt2  46297  disjf1o  46300  choicefi  46308  ioondisj2  46599  ioondisj1  46600  lptioo2  46737  lptioo1  46738  0ellimcdiv  46753  liminflbuz2  46919  ioodvbdlimc1  47037  ioodvbdlimc2  47039  stoweidlem31  47135  stoweidlem59  47163  wallispilem4  47172  wallispi  47174  stirlinglem3  47180  stirlinglem14  47191  dirkerper  47200  dirkertrigeq  47205  dirkercncflem2  47208  fourierdlem4  47215  fourierdlem30  47241  fourierdlem41  47252  fourierdlem42  47253  fourierdlem44  47255  fourierdlem46  47256  fourierdlem48  47258  fourierdlem49  47259  fourierdlem62  47272  fourierdlem74  47284  fourierdlem75  47285  fourierdlem79  47289  fourierdlem102  47312  fourierdlem114  47324  fouriersw  47335  elaa2lem  47337  elaa2  47338  etransclem24  47362  etransclem44  47382  etransclem47  47385  ioorrnopnlem  47408  subsaliuncl  47462  sge0cl  47485  meadjun  47566  meadjiunlem  47569  hoicvr  47652  ovnsubadd2lem  47749  smflimlem6  47880  smfpimcc  47912  smflimsuplem2  47925  sqrtnnaa  48007  sqrtnzqaa  48008  cjnpoly  48033  modm2nep1  48536  modm1nep2  48538  modm1p1ne  48540  lswn0  48620  sprvalpwn0  48659  fmtnoprmfac1lem  48743  grimuhgr  49079  gpg3nbgrvtx0  49268  el0ldep  49672  islindeps2  49689  ldepsnlinclem1  49711  ldepsnlinclem2  49712  itscnhlinecirc02plem1  49988  ovconstbrd  50067  ovconstbrn0d  50068  catprs  50219  fucofvalne  50541  crosspv2d  51130  crosspv3d  51131