MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqnetrd Structured version   Visualization version   GIF version

Theorem eqnetrd 3081
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
StepHypRef Expression
1 eqnetrd.2 . 2 (𝜑𝐵𝐶)
2 eqnetrd.1 . . 3 (𝜑𝐴 = 𝐵)
32neeq1d 3073 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 259 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wne 3014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-ne 3015
This theorem is referenced by:  eqnetrrd  3082  3netr4d  3091  opnz  5356  xpdifid  6018  undefne0  7937  onoviun  7972  intrnfi  8872  cantnfp1lem2  9134  cantnfp1lem3  9135  wemapwe  9152  acndom2  9472  fin23lem14  9747  fin23lem40  9765  isf32lem6  9772  isf34lem5  9792  isf34lem7  9793  isf34lem6  9794  axcc2lem  9850  xaddnemnf  12621  xaddnepnf  12622  fseqsupcl  13337  hashprg  13748  elprchashprn2  13749  hash1n0  13774  limsupgre  14830  isercolllem3  15015  prodfn0  15242  ntrivcvgtail  15248  fproddiv  15307  fprodn0  15325  tanval3  15479  tanneg  15493  ruclem11  15585  bezoutr1  15905  phibndlem  16099  dfphi2  16103  0ram  16348  0ram2  16349  ram0  16350  0ramcl  16351  gsumval2  17888  sgrp2nmndlem5  18086  issubg2  18286  ghmrn  18363  pmtrmvd  18576  gsumval3  19019  pgpfaclem2  19196  ablfaclem2  19200  ablfaclem3  19201  fincygsubgodd  19226  subdrgint  19574  abvdom  19601  lbsextlem2  19923  gzrngunit  20603  zringunit  20627  cnmsgnsubg  20713  frlmssuvc2  20931  iinopn  21502  cnconn  22022  1stcfb  22045  dissnlocfin  22129  fbasrn  22484  fclscmpi  22629  alexsublem  22644  ustuqtop5  22846  cnextucn  22904  dscmet  23174  reperflem  23418  evth  23555  cmetcaulem  23883  iscmet3  23888  metsscmetcld  23910  cmetss  23911  bcthlem5  23923  bcth2  23925  mbflimsup  24259  itg1addlem4  24292  itg1climres  24307  itg2monolem1  24343  itg2i1fseq2  24349  tdeglem4  24646  deg1add  24689  deg1mul2  24700  deg1tm  24704  dgreq  24826  dgradd2  24850  dgrmul  24852  dgrmulc  24853  dgrcolem1  24855  plyrem  24886  facth  24887  fta1lem  24888  vieta1lem1  24891  vieta1lem2  24892  vieta1  24893  qaa  24904  aareccl  24907  geolim3  24920  aaliou3lem9  24931  coseq00topi  25080  cosne0  25106  tanord  25114  tanarg  25194  cxpne0  25252  cxpsqrt  25278  logbrec  25352  chordthmlem  25402  chordthmlem2  25403  dcubic  25416  mcubic  25417  cubic2  25418  cubic  25419  quartlem4  25430  atandmneg  25476  atandmcj  25479  atancj  25480  atanrecl  25481  atanlogsublem  25485  efiatan2  25487  tanatan  25489  atandmtan  25490  cosatan  25491  cosatanne0  25492  wilthlem2  25638  ftalem7  25648  basellem2  25651  basellem4  25653  basellem5  25654  isppw  25683  dchrptlem2  25833  lgsne0  25903  2sqlem8a  25993  2sqlem8  25994  tglnpt2  26419  midexlem  26470  colperpexlem3  26510  mideulem2  26512  lnopp2hpgb  26541  subgruhgredgd  27058  wwlksnext  27663  wspthsnonn0vne  27688  clwwisshclwws  27785  vdn0conngrumgrv2  27967  vdgn1frgrv2  28067  imadifxp  30343  acunirnmpt  30396  fnpreimac  30408  xaddeq0  30469  pmtrcnelor  30728  qsidomlem2  30959  madjusmdetlem2  31086  xrge0iifhom  31173  signswn0  31823  signsvtn0  31833  signstfvneq0  31835  repr0  31875  derangenlem  32411  subfacp1lem3  32422  subfacp1lem5  32424  wsuclem  33105  noseponlem  33164  ivthALT  33676  neibastop1  33700  finxpreclem2  34663  finxpreclem6  34669  tan2h  34876  poimirlem9  34893  heicant  34919  itg2addnclem2  34936  lsatfixedN  36137  islshpat  36145  lkrshp  36233  2llnm3N  36697  dalemdnee  36794  cdleme18b  37420  cdleme40m  37595  cdlemg12g  37777  cdlemh  37945  cdlemj3  37951  tendoconid  37957  cdlemk3  37961  cdlemk12  37978  cdlemk12u  38000  cdlemk46  38076  cdlemk54  38086  erngdvlem4  38119  erngdvlem4-rN  38127  dibn0  38281  dihglblem2aN  38421  dochshpncl  38512  dochsnnz  38578  dochsatshpb  38580  lcfl7lem  38627  lcfl8b  38632  lcfrlem33  38703  lcfr  38713  hdmaprnlem3uN  38979  nn0rppwr  39172  remul01  39227  remulinvcom  39238  3cubeslem2  39272  cmpfiiin  39284  pell1234qrne0  39440  rmxyneg  39507  fnwe2lem2  39641  kelac1  39653  wnefimgd  40502  radcnvrat  40636  binomcxplemfrat  40673  binomcxplemradcnv  40674  disjrnmpt2  41438  disjf1o  41441  choicefi  41452  ioondisj2  41756  ioondisj1  41757  lptioo2  41901  lptioo1  41902  0ellimcdiv  41919  liminflbuz2  42085  ioodvbdlimc1  42207  ioodvbdlimc2  42209  stoweidlem31  42306  stoweidlem59  42334  wallispilem4  42343  wallispi  42345  stirlinglem3  42351  stirlinglem14  42362  dirkerper  42371  dirkertrigeq  42376  dirkercncflem2  42379  fourierdlem4  42386  fourierdlem30  42412  fourierdlem41  42423  fourierdlem42  42424  fourierdlem44  42426  fourierdlem46  42427  fourierdlem48  42429  fourierdlem49  42430  fourierdlem62  42443  fourierdlem74  42455  fourierdlem75  42456  fourierdlem79  42460  fourierdlem102  42483  fourierdlem114  42495  fouriersw  42506  elaa2lem  42508  elaa2  42509  etransclem24  42533  etransclem44  42553  etransclem47  42556  ioorrnopnlem  42579  subsaliuncl  42631  sge0cl  42653  meadjun  42734  meadjiunlem  42737  hoicvr  42820  ovnsubadd2lem  42917  smflimlem6  43042  smfpimcc  43072  smflimsuplem2  43085  lswn0  43594  sprvalpwn0  43635  fmtnoprmfac1lem  43716  el0ldep  44511  islindeps2  44528  ldepsnlinclem1  44550  ldepsnlinclem2  44551  itscnhlinecirc02plem1  44759
  Copyright terms: Public domain W3C validator