Theorem eqnetrd 2691

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetrd.1	|- ( ph -> A = B )
eqnetrd.2	|- ( ph -> B =/= C )

Assertion

Ref	Expression
eqnetrd	|- ( ph -> A =/= C )

Proof of Theorem eqnetrd

Step	Hyp	Ref	Expression
1		eqnetrd.2	. 2 |- ( ph -> B =/= C )
2		eqnetrd.1	. . 3 |- ( ph -> A = B )
3	2	neeq1d 2683	. 2 |- ( ph -> ( A =/= C <-> B =/= C ) )
4	1, 3	mpbird 236	1 |- ( ph -> A =/= C )

Syntax hints:   -> wi 4   = wceq 1444   =/= wne 2622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444  df-ne 2624

This theorem is referenced by:  eqnetrrd  2692  3netr4d  2701  opnz  4673  frsn  4905  xpdifid  5265  undefne0  7026  onoviun  7062  intrnfi  7930  cantnfp1lem2  8184  cantnfp1lem3  8185  wemapwe  8202  acndom2  8485  fin23lem14  8763  fin23lem40  8781  isf32lem6  8788  isf34lem5  8808  isf34lem7  8809  isf34lem6  8810  axcc2lem  8866  xaddnemnf  11527  xaddnepnf  11528  fseqsupcl  12190  hashprg  12572  elprchashprn2  12573  limsupgre  13542  limsupgreOLD  13543  isercolllem3  13730  prodfn0  13950  ntrivcvgtail  13956  fproddiv  14015  fprodn0  14033  tanval3  14188  tanneg  14202  ruclem11  14292  phibndlem  14718  dfphi2  14722  0ram  14978  0ram2  14979  ram0  14980  0ramcl  14981  gsumval2  16523  sgrp2nmndlem5  16663  issubg2  16832  ghmrn  16896  pmtrmvd  17097  gsumval3  17541  pgpfaclem2  17715  ablfaclem2  17719  ablfaclem3  17720  abvdom  18066  lbsextlem2  18382  gzrngunit  19033  zringunit  19062  cnmsgnsubg  19145  frlmssuvc2  19353  iinopn  19932  cnconn  20437  1stcfb  20460  dissnlocfin  20544  fbasrn  20899  fclscmpi  21044  alexsublem  21059  ustuqtop5  21260  cnextucn  21318  dscmet  21587  reperflem  21836  evth  21987  cmetcaulem  22258  iscmet3  22263  cmetss  22284  bcthlem5  22296  bcth2  22298  mbflimsup  22623  mbflimsupOLD  22624  itg1addlem4  22657  itg1climres  22672  itg2monolem1  22708  itg2i1fseq2  22714  tdeglem4  23009  deg1add  23052  deg1mul2  23063  deg1tm  23067  dgreq  23198  dgradd2  23222  dgrmul  23224  dgrmulc  23225  dgrcolem1  23227  plyrem  23258  facth  23259  fta1lem  23260  vieta1lem1  23263  vieta1lem2  23264  vieta1  23265  qaa  23279  aareccl  23282  geolim3  23295  aaliou3lem9  23306  coseq00topi  23457  cosne0  23479  tanord  23487  tanarg  23568  cxpne0  23622  cxpsqrt  23648  logbrec  23719  chordthmlem  23758  chordthmlem2  23759  dcubic  23772  mcubic  23773  cubic2  23774  cubic  23775  quartlem4  23786  atandmneg  23832  atandmcj  23835  atancj  23836  atanrecl  23837  atanlogsublem  23841  efiatan2  23843  tanatan  23845  atandmtan  23846  cosatan  23847  cosatanne0  23848  wilthlem2  23994  ftalem7  24005  basellem2  24008  basellem4  24010  basellem5  24011  isppw  24041  dchrptlem2  24193  lgsne0  24261  2sqlem8a  24299  2sqlem8  24300  tglnpt2  24686  midexlem  24737  colperpexlem3  24774  mideulem2  24776  lnopp2hpgb  24805  edgwlk  25259  wwlknext  25452  vdn0frgrav2  25751  vdgn0frgrav2  25752  vdn1frgrav2  25753  vdgn1frgrav2  25754  imadifxp  28212  acunirnmpt  28261  nn0sqeq1  28324  xaddeq0  28330  madjusmdetlem2  28654  xrge0iifhom  28743  signswn0  29449  signsvtn0  29459  signstfvneq0  29461  derangenlem  29894  subfacp1lem3  29905  subfacp1lem5  29907  wsuclem  30508  noseponlem  30555  nobndlem8  30588  ivthALT  30991  neibastop1  31015  finxpreclem2  31782  finxpreclem6  31788  tan2h  31937  poimirlem9  31949  heicant  31975  itg2addnclem2  31994  lsatfixedN  32575  islshpat  32583  lkrshp  32671  2llnm3N  33134  dalemdnee  33231  cdleme18b  33858  cdleme40m  34034  cdlemg12g  34216  cdlemh  34384  cdlemj3  34390  tendoconid  34396  cdlemk3  34400  cdlemk12  34417  cdlemk12u  34439  cdlemk46  34515  cdlemk54  34525  erngdvlem4  34558  erngdvlem4-rN  34566  dibn0  34721  dihglblem2aN  34861  dochshpncl  34952  dochsnnz  35018  dochsatshpb  35020  lcfl7lem  35067  lcfl8b  35072  lcfrlem33  35143  lcfr  35153  hdmaprnlem3uN  35422  cmpfiiin  35539  pell1234qrne0  35699  rmxyneg  35768  bezoutr1  35836  fnwe2lem2  35909  kelac1  35921  wnefimgd  36600  radcnvrat  36663  binomcxplemfrat  36700  binomcxplemradcnv  36701  disjrnmpt2  37463  disjf1o  37466  choicefi  37481  ioondisj2  37589  ioondisj1  37590  lptioo2  37711  lptioo1  37712  0ellimcdiv  37730  ioodvbdlimc1  37807  ioodvbdlimc2  37810  stoweidlem31  37892  stoweidlem59  37920  wallispilem4  37930  wallispi  37932  stirlinglem3  37938  stirlinglem14  37949  dirkerper  37958  dirkertrigeq  37963  dirkercncflem2  37966  fourierdlem4  37973  fourierdlem30  37999  fourierdlem41  38011  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem44  38015  fourierdlem46  38016  fourierdlem48  38018  fourierdlem49  38019  fourierdlem62  38032  fourierdlem74  38044  fourierdlem75  38045  fourierdlem79  38049  fourierdlem102  38072  fourierdlem114  38084  fouriersw  38095  elaa2lem  38097  elaa2lemOLD  38098  elaa2  38099  etransclem24  38123  etransclem44  38143  etransclem47  38146  sge0cl  38223  meadjun  38300  meadjiunlem  38303  hoicvr  38370  lswn0  38920  pfxn0  38935  hash1n0  39069  subgruhgredgd  39356  el0ldep  40312  islindeps2  40329  ldepsnlinclem1  40351  ldepsnlinclem2  40352