Theorem eqnetrd 2710

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 2702	. 2 |- ( ph -> ( A =/= C <-> B =/= C ) )
4	1, 3	mpbird 240	1 |- ( ph -> A =/= C )

Syntax hints:   -> wi 4   = wceq 1452   =/= wne 2641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-cleq 2464  df-ne 2643

This theorem is referenced by:  eqnetrrd  2711  3netr4d  2720  opnz  4673  frsn  4910  xpdifid  5271  undefne0  7044  onoviun  7080  intrnfi  7948  cantnfp1lem2  8202  cantnfp1lem3  8203  wemapwe  8220  acndom2  8503  fin23lem14  8781  fin23lem40  8799  isf32lem6  8806  isf34lem5  8826  isf34lem7  8827  isf34lem6  8828  axcc2lem  8884  xaddnemnf  11551  xaddnepnf  11552  fseqsupcl  12228  hashprg  12610  elprchashprn2  12611  limsupgre  13619  limsupgreOLD  13620  isercolllem3  13807  prodfn0  14027  ntrivcvgtail  14033  fproddiv  14092  fprodn0  14110  tanval3  14265  tanneg  14279  ruclem11  14369  phibndlem  14797  dfphi2  14801  0ram  15057  0ram2  15058  ram0  15059  0ramcl  15060  gsumval2  16601  sgrp2nmndlem5  16741  issubg2  16910  ghmrn  16974  pmtrmvd  17175  gsumval3  17619  pgpfaclem2  17793  ablfaclem2  17797  ablfaclem3  17798  abvdom  18144  lbsextlem2  18460  gzrngunit  19110  zringunit  19139  cnmsgnsubg  19222  frlmssuvc2  19430  iinopn  20009  cnconn  20514  1stcfb  20537  dissnlocfin  20621  fbasrn  20977  fclscmpi  21122  alexsublem  21137  ustuqtop5  21338  cnextucn  21396  dscmet  21665  reperflem  21914  evth  22065  cmetcaulem  22336  iscmet3  22341  cmetss  22362  bcthlem5  22374  bcth2  22376  mbflimsup  22702  mbflimsupOLD  22703  itg1addlem4  22736  itg1climres  22751  itg2monolem1  22787  itg2i1fseq2  22793  tdeglem4  23088  deg1add  23131  deg1mul2  23142  deg1tm  23146  dgreq  23277  dgradd2  23301  dgrmul  23303  dgrmulc  23304  dgrcolem1  23306  plyrem  23337  facth  23338  fta1lem  23339  vieta1lem1  23342  vieta1lem2  23343  vieta1  23344  qaa  23358  aareccl  23361  geolim3  23374  aaliou3lem9  23385  coseq00topi  23536  cosne0  23558  tanord  23566  tanarg  23647  cxpne0  23701  cxpsqrt  23727  logbrec  23798  chordthmlem  23837  chordthmlem2  23838  dcubic  23851  mcubic  23852  cubic2  23853  cubic  23854  quartlem4  23865  atandmneg  23911  atandmcj  23914  atancj  23915  atanrecl  23916  atanlogsublem  23920  efiatan2  23922  tanatan  23924  atandmtan  23925  cosatan  23926  cosatanne0  23927  wilthlem2  24073  ftalem7  24084  basellem2  24087  basellem4  24089  basellem5  24090  isppw  24120  dchrptlem2  24272  lgsne0  24340  2sqlem8a  24378  2sqlem8  24379  tglnpt2  24765  midexlem  24816  colperpexlem3  24853  mideulem2  24855  lnopp2hpgb  24884  edgwlk  25338  wwlknext  25531  vdn0frgrav2  25830  vdgn0frgrav2  25831  vdn1frgrav2  25832  vdgn1frgrav2  25833  imadifxp  28288  acunirnmpt  28336  nn0sqeq1  28399  xaddeq0  28405  madjusmdetlem2  28728  xrge0iifhom  28817  signswn0  29521  signsvtn0  29531  signstfvneq0  29533  derangenlem  29966  subfacp1lem3  29977  subfacp1lem5  29979  wsuclem  30579  noseponlem  30626  nobndlem8  30659  ivthALT  31062  neibastop1  31086  finxpreclem2  31852  finxpreclem6  31858  tan2h  32001  poimirlem9  32013  heicant  32039  itg2addnclem2  32058  lsatfixedN  32646  islshpat  32654  lkrshp  32742  2llnm3N  33205  dalemdnee  33302  cdleme18b  33929  cdleme40m  34105  cdlemg12g  34287  cdlemh  34455  cdlemj3  34461  tendoconid  34467  cdlemk3  34471  cdlemk12  34488  cdlemk12u  34510  cdlemk46  34586  cdlemk54  34596  erngdvlem4  34629  erngdvlem4-rN  34637  dibn0  34792  dihglblem2aN  34932  dochshpncl  35023  dochsnnz  35089  dochsatshpb  35091  lcfl7lem  35138  lcfl8b  35143  lcfrlem33  35214  lcfr  35224  hdmaprnlem3uN  35493  cmpfiiin  35610  pell1234qrne0  35770  rmxyneg  35839  bezoutr1  35907  fnwe2lem2  35980  kelac1  35992  wnefimgd  36671  radcnvrat  36733  binomcxplemfrat  36770  binomcxplemradcnv  36771  disjrnmpt2  37534  disjf1o  37537  choicefi  37552  ioondisj2  37685  ioondisj1  37686  lptioo2  37808  lptioo1  37809  0ellimcdiv  37827  ioodvbdlimc1  37904  ioodvbdlimc2  37907  stoweidlem31  38004  stoweidlem59  38032  wallispilem4  38042  wallispi  38044  stirlinglem3  38050  stirlinglem14  38061  dirkerper  38070  dirkertrigeq  38075  dirkercncflem2  38078  fourierdlem4  38085  fourierdlem30  38111  fourierdlem41  38123  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem44  38127  fourierdlem46  38128  fourierdlem48  38130  fourierdlem49  38131  fourierdlem62  38144  fourierdlem74  38156  fourierdlem75  38157  fourierdlem79  38161  fourierdlem102  38184  fourierdlem114  38196  fouriersw  38207  elaa2lem  38209  elaa2lemOLD  38210  elaa2  38211  etransclem24  38235  etransclem44  38255  etransclem47  38258  sge0cl  38337  meadjun  38416  meadjiunlem  38419  hoicvr  38488  ovnsubadd2lem  38585  lswn0  39067  pfxn0  39082  hash1n0  39219  subgruhgredgd  39520  el0ldep  40767  islindeps2  40784  ldepsnlinclem1  40806  ldepsnlinclem2  40807